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

[Noam Zeilberger]

Yes, that must be the issue, thanks!  Reproduced the behavior below:

data A : Set where
  binary : (l : A) → (r : A) → A
  ternary : (l : A) → (m : A) → (r : A) → A

data B : Set where
  binary : (l : A) → (r : A) → B
  ternary : (l : A) → (m : A) → (r : A) → B

f : A → A
f (binary x x₁) = {!!}
f (ternary x x₁ x₂) = {!!}

g : B → B
g (binary l r) = {!!}
g (ternary l m r) = {!!}



On Thu, 14 Feb 2019 at 20:46, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190214/663bba60/attachment.html>