[Agda] Argument order, universes and erasability

Nils Anders Danielsson nad at cse.gu.se
Tue Oct 15 07:38:40 CEST 2013


On 2013-10-13 16:59, Mathijs Kwik wrote:
> Am I correct in this assumption? Or is reality far more complicated? :)

The Epic backend contains some erasure optimisations. See the following
release notes:

* http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-10
* http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-3-0

-- 
/NAD


More information about the Agda mailing list