[Agda] Argument order, universes and erasability

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

Previous message: [Agda] Argument order, universes and erasability
Next message: [Agda] Call for Talk Proposals: Data-Centric Programming, San Diego, Jan 2014
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

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

Previous message: [Agda] Argument order, universes and erasability
Next message: [Agda] Call for Talk Proposals: Data-Centric Programming, San Diego, Jan 2014
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the Agda mailing list