[Agda] Tricks to limit the memory consumption?

[gallais at EnsL.org]

Hi everyone,

I am currently gluing all the pieces together in order to (finally)
finish my solver
for Presburger arithmetic in Agda. The only problem I am not able to address
is the memory that it takes to typecheck the last theorems.

Here are the few tricks that I used and that allowed me to typecheck more
theorems before hitting the wall of memory consumption:
- use « open import ... using ... » in order to avoid loading too much lemmas
- use « abstract » in order to use opaque terms

Are these tricks really useful (especially the one involving « using » because I
actually saw the efficiency of « abstract »)? Are there other tricks
that I could
use to get more theorems typechecked?

Thank you for providing Agda: it's a pleasure to play with it!
Cheers,

--
guillaume