[Agda] Telescope syntax

[Matthieu Sozeau]

Hi, 

  It seems you’re gonna have to invent names for the i’s… 
Coq has a similar feature using a generalizable variables syntax 
whereby you can declare some names to be generalized (e.g. A B i j k) 
and then writing `(X : Type i) will add an implicit {i} binder just before
(x : Type i). The backquote can actually be put anywhere and will introduce
pi’s or lambdas according to whether we’re in type or (term or unknown) 
position for the generalizable variable occurrences appearing in it’s scope. 
It was introduced for type class instance arguments mainly, allowing 
compact `{Eq A} binders for example. It can also introduce automagically named 
binders for superclasses but it’s seldom used. I just want to point out that
if you allow this then further references to constants using telsyntax
should probably not be allowed to refer to the generated names :)

Best,
— Matthieu

On 26 nov. 2014, at 22:11, Andy Morris <andy at adradh.org.uk> wrote:

> 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