[Agda] Telescope syntax

[Guillaume Brunerie]

Oh, I see, I forgot that "syntax" provides the syntax of a specific
identifier (I don’t use it very often).
Good, we can have it in the forward direction then :)

2014-11-27 11:05 GMT+01:00 Ulf Norell <ulf.norell at gmail.com>:
> 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
>>
>