[Agda] Syntax declarations

[Ulf Norell]

On Sun, Mar 18, 2018 at 8:50 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> The design seems backward to me, but I suspect there are good reasons why
> it is the way it is. It would help me to understand syntax declarations if
> I knew what they are, but the note cited doesn't explain.
>

The main reason for it being this way around it that it means we don't need
a separate kind of entity of syntaxes for the scope checker to manage,
which simplified the implementation quite a lot.

It also (sort of) matches the way mixfix operators work: the fact that you
can write `x + y` for `_+_ x y` is a property of the name `_+_` and not a
separate entity that may or may not be in scope.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180319/0eee9a55/attachment.html>