[Agda] evaluation in compilation

[Nils Anders Danielsson]

On 2012-10-03 16:35, Serge D. Mechveliani wrote:
> Why do the developers talk of slowness, of call by name?
> Does this refer only to evaluation during compilation?

Call-by-name is (currently) used by the type-checker. The MAlonzo
backend uses whatever GHC uses. (If we wanted to we could add lots of
strictness annotations, but this is not done at the moment.)

-- 
/NAD