<br><div class="gmail_quote">On Fri, Sep 10, 2010 at 7:21 PM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div class="im">On Friday 10 September 2010 11:33:27 am Jean-Philippe Bernardy wrote:<br>
<br>
> What you can currently do is only to swap the order of arguments to a<br>
> function:<br>
><br>
> syntax identity A a = a :: A<br>
<br>
</div>I'm quite excited at the prospect of finally having this kind of flexibility.<br>
One question I have though is: does this new system separate the sugared<br>
notation from the actual definitions, Coq-style? I've been of the opinion that<br>
one of the nice things about the current mixfix stuff was the ability to use<br>
the notations pervasively. For instance, if I'm specifying the denotation of<br>
some syntax, I can write:<br>
<br>
[_] : Syn -> Sem<br>
[ ap f x ] = ... [ f ] ... [ x ] ...<br>
[ lam e ] = ...<br>
...<br>
<br>
Which, of course, looks like the definitions you'd see in a paper or<br>
something. I think in Coq, the best one can do is something like:<br>
<br>
den : Syn -> Sem<br>
den (ap f x) = ... [ f ] ... [ x ] ...<br>
den (lam e) = ...<br>
...<br>
<br>
syntax den t = [ t ]<br>
<br>
where you're allowed to use the notation on the right, but not the left.<br>
<br>
Pattern matching on mixfix constructors would be another concern.<br>
<br>
Of course, adding binders and such is enough of a step forward that I'd give<br>
up the above. But, I'd still probably miss it from time to time.<br></blockquote><div><br>Agda isn't Coq :-). None of the old stuff is going away. The syntax declarations<br>work the same way as the current infix declarations, so they'll be in effect both<br>
on the left and on the right (of course, the binding syntax won't work on the left<br>since you can't match on lambdas).<br><br>/ Ulf<br> </div></div>