<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Hi,<div><br></div><div>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.</div><div><br></div><div>As a stop gap I am using </div><div><div>{-# OPTIONS --type-in-type #-}</div></div><div><br></div><div>It is usually easy to see wether your definitions can be stratified. </div><div><br></div><div>Cheers,</div><div>Thorsten</div><div><br></div><div><div><div>On 19 Nov 2009, at 18:41, Edward Kmett wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">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> _______________________________________________<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">https://lists.chalmers.se/mailman/listinfo/agda</a><br></blockquote></div><br></div></body><br/>
<p>
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.
</p>
</html>