[Agda] Telescope syntax

[Guillaume Brunerie]

I'm not sure what you mean. When using (X : Type) in my proposed syntax,
you don't give a name to the i, hence it will be autogenerated by Agda so
there will be no way to refer back to it by name.
What you can do instead if you need the level somewhere, is to define the
following function:

get-level : (X : Type) -> Level
get-level {i} _ = i

And then [get-level X] returns the universe level of X.

Also, in Coq why do you have to give specific names to be generalized? Why
not generalize every variable which is not in scope?

Le 27 nov. 2014 00:07, "Matthieu Sozeau" <matthieu.sozeau at gmail.com> a
écrit :
>
> 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
>
> _______________________________________________
> 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/2bbbfedd/attachment.html