[Agda] Mixfix binders: first patch

[Ulf Norell]

On Mon, Sep 13, 2010 at 3:39 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk>wrote:

> 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.
>

Yes, that seems to be the most sensible option. That way naming your
function _+_  can be seen as shorthand for

syntax _+_ x y = x + y

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