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

[Guillaume Brunerie]

I think that this feature only works for non-recursive arguments.
See the bug report https://github.com/agda/agda/issues/3214.

Best,
Guillaume

Den tors 14 feb. 2019 kl 21:02 skrev Noam Zeilberger
<noam.zeilberger at gmail.com>:
>
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda