<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Thanks Wouter, Oleg Grenrus also just told me about this feature, which seems very intuitive.</div><div><br></div><div>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></div><div><br></div><div>  foo (binary x x₁) = {!!}<br>  foo (ternary x x₁ x₂) = {!!}<br><br></div><div>Is this a feature which was added after 2.5.4.2?</div><div><br></div><div>Noam<br></div></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 14 Feb 2019 at 19:55, Swierstra, W.S. (Wouter) <<a href="mailto:W.S.Swierstra@uu.nl">W.S.Swierstra@uu.nl</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">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>
</blockquote></div>