[Agda] how does BUILTIN work - practical programming in Agda

Nils Anders Danielsson nad at chalmers.se
Mon Dec 5 20:19:27 CET 2011


On 2011-12-05 19:02, Nils Anders Danielsson wrote:
> Note that with this approach the type-checker is free to reduce seqs,
> because the reduction removes the thunk.

This argument seems to be incorrect. Besides, does anyone use seq in a
strict language?

-- 
/NAD


More information about the Agda mailing list