On 2012-10-15 14:06, Amr Sabry wrote: > I would prefer to have one entry point to the Agda code that is unsafe > as far as Agda is concerned but trusted because the user does validation > on the other side. This doesn't seem to match the current FFI very well. We haven't put a lot of effort into the FFI, so better designs are most likely possible. -- /NAD