[Agda] Mixfix binders: first patch

[Ulf Norell]

On Fri, Sep 10, 2010 at 7:21 PM, Dan Doel <dan.doel at gmail.com> wrote:

> On Friday 10 September 2010 11:33:27 am Jean-Philippe Bernardy wrote:
>
> > What you can currently do is only to swap the order of arguments to a
> > function:
> >
> > syntax identity A a = a :: A
>
> I'm quite excited at the prospect of finally having this kind of
> flexibility.
> One question I have though is: does this new system separate the sugared
> notation from the actual definitions, Coq-style? I've been of the opinion
> that
> one of the nice things about the current mixfix stuff was the ability to
> use
> the notations pervasively. For instance, if I'm specifying the denotation
> of
> some syntax, I can write:
>
>  [_] : Syn -> Sem
>  [ ap f x ] = ... [ f ] ... [ x ] ...
>  [ lam  e ] = ...
>  ...
>
> Which, of course, looks like the definitions you'd see in a paper or
> something. I think in Coq, the best one can do is something like:
>
>  den : Syn -> Sem
>  den (ap f x) = ... [ f ] ... [ x ] ...
>  den (lam  e) = ...
>  ...
>
>  syntax den t = [ t ]
>
> where you're allowed to use the notation on the right, but not the left.
>
> Pattern matching on mixfix constructors would be another concern.
>
> Of course, adding binders and such is enough of a step forward that I'd
> give
> up the above. But, I'd still probably miss it from time to time.
>

Agda isn't Coq :-). None of the old stuff is going away. The syntax
declarations
work the same way as the current infix declarations, so they'll be in effect
both
on the left and on the right (of course, the binding syntax won't work on
the left
since you can't match on lambdas).

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100910/c2d00fe5/attachment.html