[Agda] evaluation in compilation

[Serge D. Mechveliani]

On Mon, Oct 01, 2012 at 01:57:45PM +0200, Nils Anders Danielsson wrote:
> On 2012-10-01 12:34, Serge D. Mechveliani wrote:
>> Please, how to prevent a compilation time evaluation?
>
> There is no general, simple way to do this. If you can make sure that
> the type-checker doesn't need to normalise your definition, and the
> type-checker isn't overly "strict", then compile-time evaluation is
> hopefully avoided (when the MAlonzo backend is used).

What does this mean: "to normalise a definition" ?
How can one know whether the type-checker is overly strict?

> There is no general, simple way to do this. 

It follows then that there is no simple way to sort in practice in Agda 
a given list of naturals of length about 64000
(?)

Thanks,

------
Sergei