[Agda] Difference between two datatypes

[Nils Anders Danielsson]

On Thu, Jun 19, 2008 at 9:29 PM, Samuel Bronson <naesten at gmail.com> wrote:
>
> I hope that gets fixed soonish... it's terribly annoying...

In the last Agda Implementors' Meeting we discussed adding some form
of universe polymorphism. Concerns were raised that adding more and
more features will make the language too complicated, and it was also
questioned whether there really is a need for universe polymorphism.
However, I think that the more pragmatic of us (including,
importantly, Ulf) agreed that universe polymorphism should be added,
if done in a nice way. There are also some ideas about how to
implement it.

-- 
/NAD