[Agda] Mixfix binders: first patch

[Ulf Norell]

>
> Andreas Abel wrote:

> I find it awkward to define a a new function by
>
>>
>  def plus x x = mult2 x
>
>>
> where "an alternative expression for plus x x is mult2 x".


Nils Anders Danielsson <nad at cs.nott.ac.uk> wrote:

>
>
syntax <symbol we're defining syntax for> <bound variables> =
>  <new notation making use of the bound variables>


What you have to remember is that we're not defining new syntax
for an arbitrary piece of expression, we're defining the syntax for a
particular function symbol (what Nisse wrote above). It's not valid
(nor does it make sense) to define mult2 x to be the syntax for
plus x x. Having the new syntax on the left would lead you to believe
that you could define several different pieces of syntax for the same
symbol, which isn't the case. For instance,

-- not valid:
syntax plus x x = mult2 x
syntax plus x y = x + y

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