[Agda] evaluation in compilation

Serge D. Mechveliani mechvel at botik.ru
Mon Oct 1 12:34:00 CEST 2012


Please, how to prevent a compilation time evaluation?

In my example,  sort (f 2000)   builds a certain list of 2000 naturals 
and sorts it; `main' prints the result list.

And  Agda-2.3.0.1 + MAlonzo + lib-06  is not able to _compile_ this in 
any reasonable time. Probably this is because it tries to evaluate a 
constant list  (f 2000)  at the compilation time
(for (f 30), it is compiled fast enough).

I look into the compilation options and do not find a relevant key.
I do not know, may be I am missing something simple. 

Thanks,

------
Sergei


More information about the Agda mailing list