<div dir="ltr"><div dir="ltr"><div>Yes, that must be the issue, thanks!  Reproduced the behavior below:<br></div><div><br></div><div>data A : Set where<br>  binary : (l : A) → (r : A) → A<br>  ternary : (l : A) → (m : A) → (r : A) → A<br><br>data B : Set where<br>  binary : (l : A) → (r : A) → B<br>  ternary : (l : A) → (m : A) → (r : A) → B<br><br>f : A → A<br>f (binary x x₁) = {!!}<br>f (ternary x x₁ x₂) = {!!}<br><br>g : B → B<br>g (binary l r) = {!!}<br>g (ternary l m r) = {!!}<br></div><div><br></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 14 Feb 2019 at 20:46, Guillaume Brunerie <<a href="mailto:guillaume.brunerie@gmail.com">guillaume.brunerie@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I think that this feature only works for non-recursive arguments.<br>
See the bug report <a href="https://github.com/agda/agda/issues/3214" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/3214</a>.<br>
<br>
Best,<br>
Guillaume<br>
<br>
Den tors 14 feb. 2019 kl 21:02 skrev Noam Zeilberger<br>
<<a href="mailto:noam.zeilberger@gmail.com" target="_blank">noam.zeilberger@gmail.com</a>>:<br>
><br>
> Thanks Wouter, Oleg Grenrus also just told me about this feature, which seems very intuitive.<br>
><br>
> 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<br>
><br>
>   foo (binary x x₁) = {!!}<br>
>   foo (ternary x x₁ x₂) = {!!}<br>
><br>
> Is this a feature which was added after 2.5.4.2?<br>
><br>
> Noam<br>
><br>
> On Thu, 14 Feb 2019 at 19:55, Swierstra, W.S. (Wouter) <<a href="mailto:W.S.Swierstra@uu.nl" target="_blank">W.S.Swierstra@uu.nl</a>> wrote:<br>
>><br>
>> Hi Noam,<br>
>><br>
>> If you add spurious variable names when declaring the types of your constructors, such as:<br>
>><br>
>> >   ...<br>
>> >   binary : (l : A) → (r : A) → A<br>
>> >   ternary : (l : A) → (m : A) → (r : A) → A<br>
>><br>
>> Case splitting should produce:<br>
>><br>
>> >   foo (binary l r) = {!!}<br>
>> >   foo (ternary l m r) = {!!}<br>
>><br>
>> Or at least generate some name like l₁ if l is already in scope. Hope this helps,<br>
>><br>
>>   Wouter<br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>