On 2010-08-24 19:27, Christoph HERRMANN wrote: > Then converted the lemmas into postulates in the same file > and checking the data type went quickly. Have a look at the following thread: running out of memory in formalization of category theory http://thread.gmane.org/gmane.comp.lang.agda/1672 -- /NAD