[Agda] running out of memory in formalization of category theory

[Ulf Norell]

On Wed, Jun 2, 2010 at 10:01 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk>wrote:

> It seems that it is a feature of Agda that it will run out of memory if you
> try to formalize category theory :-)
>

It's for your own protection!

Seriously though, my suspicion is that the terms you get when formalizing
category theory get extremely
large with all the implicit stuff filled in. Being careful to maintain
sharing might help with that, but that
requires some reworking of the internals.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100603/b14753a1/attachment.html