[Agda] agda-mode question: custom variable naming strategy for case split?

[Noam Zeilberger]

Hello all, I have a very superficial question: is there an easy way of
modifying the rules that agda-mode uses for choosing variable names?

Like, say I have a type A with some constructors

  ...
  binary : A → A → A
  ternary : A → A → A → A

and I want to define a function

  foo : A → A
  foo x = ?

then case splitting on x will yield clauses of the form

  ...
  foo (binary x x₁) = {!!}
  foo (ternary x x₁ x₂) = {!!}

but what if I actually want to name the variables x1, x2, and x3, say, or
x, y, and z?  Of course I could just go ahead and rename the auto-generated
variables + C-c C-l, but this gets frustrating after a while...  It would
be nice to be able to specify a simple set of naming rules to be used
throughout an interaction.

Sorry for asking such a superficial question!

Noam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190214/29a40bdc/attachment.html>