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

[Nils Anders Danielsson]

On 2010-06-05 19:45, Nicolas Pouillard wrote:
> Throwing away these terms using an option may allow to significantly reduce
> the memory needed to type-check big developments.

Perhaps. However, the compiler does generate code for abstract blocks,
so it would not (in general) be correct to do so.

> This seems counter intuitive. I makes more sense and would fit nicely
> with submodules to have each abstract block independent.

Sometimes later abstract definitions depend on the actual definitions of
earlier abstract definitions. In that case it can be quite convenient
not to have to write all abstract definitions in a single block.

By the way, I checked and it seems as if abstract blocks in submodules
are independent, as you would hope.

--
/NAD