[Agda] AIM 10 notes

[Ulf Norell]

On Sun, Sep 20, 2009 at 8:20 PM, Robin Green <greenrd at greenrd.org> wrote:

> At Sat, 19 Sep 2009 22:53:35 +0200,
> Patrik Jansson wrote:
> >
> > AIM 10 is over but some notes and slides have been collected on the wiki:
> >
> >   http://wiki.portal.chalmers.se/agda/Main.AIMX
>
> On universe polymorphism it is written:
>
>     postulate
>       ↑_ : ∀ {n} Set n → Set (suc n)
>       ⇑_ : ∀ {n}{A : Set n} → A → ↑ A
>       ⇓_ : ∀ {n}{A : Set n} → ↑ A → A
>
> Are these going to be actual postulates, or are they going to be
> (at least, in the case of the first two postulates)
> automatically-applied implicit rules?


The last two will be implicit rules. The first one will be explicit in the
first version, since that simplifies the implementation somewhat. I don't
believe having to be explicit about the liftings is a big deal, but I guess
we'll find out once people start playing around with it. I'm hoping to push
this to the development version some time during the week.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090921/c151db84/attachment.html