[Agda] evaluation in compilation

[Nils Anders Danielsson]

On 2012-10-01 18:51, Serge D. Mechveliani wrote:
> *** How to prevent this evaluation in compilation time? ***

One option is to avoid hard-coded constants, and read data from a file.

> n = 16000  -- 32000

I think this number will be represented using 16001 constructors (plus
lots of uses of unsafeCoerce). The Epic backend automatically detects
that certain types can be represented using "big integers". We should
generalise this functionality and make it available to more backends.

This could be a good code sprint for someone at the Agda meeting that
starts on Wednesday.

-- 
/NAD