[Agda] evaluation in compilation

[Nils Anders Danielsson]

On 2012-10-01 19:14, Serge D. Mechveliani wrote:
> What does this mean: "to normalise a definition" ?

To evaluate it to normal form.

> How can one know whether the type-checker is overly strict?

This is somewhat subjective. I can give you one example. If you write

   n : ℕ
   n = f 3,

and n is not used elsewhere in the file, then there is no need for the
type-checker to normalise n. On the other hand, if you write

   foo : f 3 ≡ pred (suc _)
   foo = refl,

then I think it is very reasonable for Agda to normalise both sides of
the equality and instantiate the underscore to the normal form of f 3.

To see what has been normalised you can inspect the generated Haskell
code.

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

As I wrote elsewhere: You can work around this problem by reading (parts
of) the input from a file. Furthermore I suspect that your problem is
not related to normalisation but rather to the representation of natural
numbers.

-- 
/NAD