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

[Alan Jeffrey]

On 12/05/2011 03:57 AM, Andreas Abel wrote:
> Of course, on the long run, we may agree on a minimum set of primitives
> each compiler has to implement, that covers at least arithmetic.

JS is problematic for this, as there's no native bignum type, so we'd 
have to pick a bignum library to link against. I'm a bit loath to 
hard-wire such a library into the compiler, rather than allowing 
developers to choose which library to link against.

> Cheers,
> Andreas

A.