[Agda] Agda interface generation memory consumption

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Fri Feb 12 15:33:35 CET 2010


On 2010-02-10 21:02, Dan Doel wrote:
> I don't have a solution, but I have an additional 'test case' if the
> implementers want one, although it's essentially the same one as the last time
> this came up.
>
>   http://code.haskell.org/~dolio/agda-share/categorica/Category/Product.agda

We actually used your code as a test case. If we remove your previous
fix (you instantiated some implicit argument explicitly), then the code
type checks roughly four times faster using the new version of Agda.

--
/NAD


More information about the Agda mailing list