When did universe polymorphism sneak in? <br><br>The lack of it was the reason I stopped using Agda!<br><br>-Edward Kmett<br><br><div class="gmail_quote">On Thu, Nov 19, 2009 at 1:33 PM, Luke Palmer <span dir="ltr"><<a href="mailto:lrpalmer@gmail.com">lrpalmer@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">I have been diving into Agda recently, and have a decent amount of<br>
tuits. I notice that a decent amount of the standard library is not<br>
using universe polymorphism. Is there a reason for this, or is it<br>
just that nobody has got a round tuit? I'd be happy to start<br>
converting things if the latter.<br>
<br>
Luke<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br>