[Agda] Mixfix binders: first patch

[Nils Anders Danielsson]

On 2010-09-13 14:30, Jean-Philippe Bernardy wrote:
>> On a related note, is there a way to give the associativity/precedence
>> of the new notation?
>
> Fixities can already be specified for any names, so the fixity of the
> name will be used.

This seems wrong to me. Contrived example:

   _◅_ : A → List A → List A

   infixr 5 _◅_

   syntax _◅_ x xs = xs ▻ x

I would like to be able to specify that xs ▻ x ▻ y should be parsed as
(xs ▻ x) ▻ y, i.e. left associatively. I think it should be possible to
specify the fixity of the new syntax separately from that of the old.

Another option is to only allow syntax declarations for non-operator
identifiers. In this case a fixity declaration for the identifier would
apply to the syntax (and fixity declarations for non-operator
identifiers without syntax would not be allowed). I think I prefer this
option.

--
/NAD