[Agda] lists/vectors

Nils Anders Danielsson nad at chalmers.se
Mon Oct 15 23:50:13 CEST 2012

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.


More information about the Agda mailing list