[Agda] Agda's syntax declaration

[Martin Escardo]

Thanks for you answer, Ulf.

On 04/11/17 06:33, ulf.norell at gmail.com wrote:
> 
> On Fri, Nov 3, 2017 at 11:37 PM, Martin Escardo <m.escardo at cs.bham.ac.uk 
> <mailto:m.escardo at cs.bham.ac.uk>> wrote:
> 
>     Can I say some things about Agda's syntax declaration?
> 
>     * Why are the definitions backwards (what you define is in the
>     right-hand side)?
> 
> 
> They're not. You are defining the syntax for a particular name in the 
> same way that
> you define the value of a particular name (`syntax f x = bla` vs `f x = 
> bla`). If syntax
> declarations were the other way around you would be very surprised to 
> find that you
> can't have multiple syntax declarations for the same name (which you can't).

I don't understand this remark. Consider again

```
id : {A : Type} → A → A
id {A} x = x

syntax id {A} x = x ∶ A

infixl 0 id
```

In the syntax definition, I have *already* define id (occurring in the 
left-hand side), and the new thing I am *defining* in the syntax 
declaration is ":", which occurs in the *right*-hand side.

At first I tried to define ":" to be left-associative, but this didn't 
work. Then cheating from other people's examples I realized that one is 
expected to define `id` to be left-associative. I didn't answer the 
question myself as you suggest: I still don't know what it means for id 
to be left-associative. :-) The above works and is useful, but I don't 
understand it.

Best,
Martin