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

[Alan Jeffrey]

On 12/05/2011 01:19 PM, Nils Anders Danielsson wrote:
> 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?

I think the idea is to allow interoperability between strict and lazy 
implementations of Agda. In a strict implementation, seq would be a no-op.

A.