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

[Alan Jeffrey]

On 12/05/2011 10:15 AM, Nils Anders Danielsson wrote:
> On 2011-12-05 17:05, Alan Jeffrey wrote:
> I assume that there are no guarantees that evaluating 2 + 2 on the Agda
> side and on the JS side give equivalent results.

Indeed. When you hit the FFI, you are into a trusted computing base. I'm 
reasonably confident that 2 + 2 agree on both sides, but 2^60 + 2 I'm 
not so sure about.

A.