[Agda] Speeding up Agda

[Christoph HERRMANN]

Hi all,

I had problems with extremely long times for type checking;
basically a set of lemmas and a data type using them.

 Checking the lemmas alone went quickly, also having the
data type in a similar form and not using the lemmas.

I thought separate compilation could help so put the lemmas
in a file which I compiled before, but that did not help.

Then converted the lemmas into postulates in the same file
and checking the data type went quickly. Note the lemmas
have already been proved. 

Have I done something illegal or is it just a problem 
that separate compilation is not exploited for efficiency?

Cheers
--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532