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

[Noam Zeilberger]

Thanks Wouter, Oleg Grenrus also just told me about this feature, which
seems very intuitive.

However, it doesn't seem to work on my version of agda!  After adding
variable names in pi types for the constructors binary and ternary, case
splitting still gives me

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

Is this a feature which was added after 2.5.4.2?

Noam

On Thu, 14 Feb 2019 at 19:55, Swierstra, W.S. (Wouter) <W.S.Swierstra at uu.nl>
wrote:

> Hi Noam,
>
> If you add spurious variable names when declaring the types of your
> constructors, such as:
>
> >   ...
> >   binary : (l : A) → (r : A) → A
> >   ternary : (l : A) → (m : A) → (r : A) → A
>
> Case splitting should produce:
>
> >   foo (binary l r) = {!!}
> >   foo (ternary l m r) = {!!}
>
> Or at least generate some name like l₁ if l is already in scope. Hope this
> helps,
>
>   Wouter
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190214/f8c20c9f/attachment.html>