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

[Nils Anders Danielsson]

On 2010-06-04 02:28, Anton Setzer wrote:
> Could it be that the poor performance of agda is due to the fact that
> it always normalises two terms in order to compare whether they are
> equal even if they are identical.

This hypothesis has been tested (on a very small sample of code). Only a
small fraction of the equality tests were between equal terms, if I
remember correctly.

> We sometimes proved those theorems, then postulated the proofs and
> referred to the postulated proofs, just in order to avoid Agda
> normalising the proofs.

You don't need to use postulates. Use abstract instead:

   abstract

     foo : Foo
     foo = …

     bar : Bar
     bar = …

Here foo and bar are transparent within the abstract block (within all
abstract blocks in the same module, I believe ①), but opaque outside.

① I don't know how abstract blocks in submodules are treated.

--
/NAD