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

[Nils Anders Danielsson]

On 2011-12-05 17:05, Alan Jeffrey wrote:
> Rather than including specific cases for base types, the JS FFI is
> very flexible about data bindings (essentially it supports view
> patterns. Agda datatypes can be bound to any JS type you like. In
> particular, you can bind the natural numbers to raw JS numbers.

I assume that there are no guarantees that evaluating 2 + 2 on the Agda
side and on the JS side give equivalent results.

-- 
/NAD