[Agda] evaluation in compilation

[Nils Anders Danielsson]

On 2012-10-01 20:02, Serge D. Mechveliani wrote:
> 1. In practice, a large expression (not only a number) more often appears
>     not from a file but as  a result of a function,  a result of
>     intermediate computation.

This sounds like a bug.

> 2. A binary counter for the value of  b = 2^18  : Bin  has a small
>     representation. But the compiler still tries to evaluate at the
> compilation time the corresponding concatenation of 2^18 small lists
> built by a function in my example.
> By the way, if this  b  is read from a file, will this prevent this
> long compilation effect in this example?

I hope so.

-- 
/NAD