[Agda] Universe polymorphism in the standard library

[Edward Kmett]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091119/3e6af5a4/attachment.html