<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>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?</div><div><br></div><div>Like, say I have a type A with some constructors<br></div><div><br></div><div>  ...<br></div>  binary : A → A → A<br><div>  ternary : A → A → A → A<br></div><div><br></div><div>and I want to define a function</div><div><br></div><div><div>  foo : A → A<br>  foo x = ?<br></div><div><br></div></div><div>then case splitting on x will yield clauses of the form<br></div></div><div dir="ltr"><br></div><div dir="ltr">  ...<br></div><div dir="ltr">  foo (binary x x₁) = {!!}<br>  foo (ternary x x₁ x₂) = {!!}<br></div><div dir="ltr"><br></div><div>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.<br></div><br><div>Sorry for asking such a superficial question!</div><div><br></div><div>Noam<br></div></div></div></div></div></div></div>