[Agda] Typeclasses again in release-candidate/master

effectfully effectfully at gmail.com
Sat Feb 20 08:33:29 CET 2016


Ulf Norell, would it make sense to give a special treatment for level
metas wrt instance search? Records are very often parameterized by
levels and it doesn't feel good to choose between universe
polymorphism and instance search.


More information about the Agda mailing list