[Agda] Passing numerics to haskell

[Alan Jeffrey]

There's some bindings for native natural numbers hidden away in:

https://github.com/agda/agda-system-io/blob/master/src/Data/Natural.agda

plus its dependencies.  There are some gotchas, notably the naming 
scheme used by the compiler has changed between versions, so you need to 
be careful about which agda version you use to compile with.  Also, the 
optimizations used to get good performance are incredibly dependent on 
the version of the compiler.

I should really move this out from agda-system-io, but that requires 
working out a good way to get build dependencies to work.

A.

On 02/08/2011 03:41 PM, Pavel Perikov wrote:
> What is a tentative way to pass numerical values to haskell during compilation? Does any of the built in types map directly to haskell types? (Natural, Integer, Float)?
>
> pavel_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda