[Agda] Telescope syntax

[Ulf Norell]

The reason syntax declarations are 'backwards' is that they should be read
as providing the syntax for a particular identifier. For instance,

  syntax foo x y z = [ x / y ]- z

defines the syntax of foo to be the thing on the right. Having it the other
way around would give you the wrong idea of what's going on. In particular
you'd expect to be able do write things like

  syntax [ x ] = x :: []

or

  syntax [ x / y ]- z = foo x y z
  syntax [ x /]- z = foo x x z

The backwards direction doesn't make sense for the telescope syntax though.
In that case you are defining a new name (like 'Type' or 'Group') so that
should go on the left (in my opinion).

/ Ulf

On Thu, Nov 27, 2014 at 10:25 AM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> (apparently something got wrong with my previous email, trying again...)
>
> I have no idea why the "syntax" syntax is backwards, but I thought it
> would make more sense to have both of them backwards rather than having
> them in different directions.
> Le 27 nov. 2014 10:21, "Guillaume Brunerie" <guillaume.brunerie at gmail.com>
> a écrit :
>
> It's backwards the same way the current syntax declarations are, and
>>> presumably for the same reason.
>>>
>>> > On 26 Nov 2014, at 22:08, Felipe Lessa <felipe.lessa at gmail.com> wrote:
>>> >
>>> > On 26-11-2014 11:33, Guillaume Brunerie wrote:
>>> >>  telsyntax {i : Level} (X : Set i) = (X : Type)
>>> >
>>> > I hope this isn't an obvious question, but isn't this syntax backwards?
>>> > Shouldn't it be like below?
>>> >
>>> >  telsyntax (X : Type) = {i : Level} (X : Set i)
>>> >
>>> > Cheers, :)
>>> >
>>> > --
>>> > Felipe.
>>> >
>>> > _______________________________________________
>>> > Agda mailing list
>>> > Agda at lists.chalmers.se
>>> > https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141127/387440a5/attachment-0001.html