[Agda] Mixfix binders: first patch

[Dan Doel]

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.

-- Dan