[Agda] Universe polymorphism in the standard library

[Thorsten Altenkirch]

Hi,

Ulf has got an experimental implementation of universe polymorphism.  
However, I'd think it is too early to reimplement the whole library  
based on this.

As a stop gap I am using
{-# OPTIONS --type-in-type #-}

It is usually easy to see wether your definitions can be stratified.

Cheers,
Thorsten

On 19 Nov 2009, at 18:41, Edward Kmett wrote:

> When did universe polymorphism sneak in?
>
> The lack of it was the reason I stopped using Agda!
>
> -Edward Kmett
>
> On Thu, Nov 19, 2009 at 1:33 PM, Luke Palmer <lrpalmer at gmail.com>  
> wrote:
> I have been diving into Agda recently, and have a decent amount of
> tuits.  I notice that a decent amount of the standard library is not
> using universe polymorphism.  Is there a reason for this, or is it
> just that nobody has got a round tuit?  I'd be happy to start
> converting things if the latter.
>
> Luke
> _______________________________________________
> 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


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091119/b0fec257/attachment.html