[Agda] Agda's syntax declaration

[Ulf Norell]

Ok, let me try to be more precise. In your example you are defining a
single thing (id)
with multiple properties. You can read it as something like this:

```
id.TYPE = {A : Type} → A → A
id.VALUE = {A} x ↦ x
id.SYNTAX = {A} x ↦ x "∶" A
id.FIXITY = infixl 0
```

Contrary to your intuition "∶" is not a thing in its own right, but simply
a terminal symbol in
the parsing rule for id.

/ Ulf


On Sat, Nov 4, 2017 at 8:44 AM, Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171104/c85ed552/attachment.html>