[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