The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 06/30/2016 12:04 PM, Soegtrop, Michael wrote:
> Dear Laurent,
>
> as it looks I might need 4 number libraries, one for reasonably efficient 
> safe computation in Coq, one for fast not so safe computation in Coq, another 
> one optimized for OCaml export and maybe yet another one which concentrates 
> on simplicity to help beginners to understand the interface.
>
> E.g. an Int32 type is probably best mapped to an OCaml Int32 and not to a 
> BigN using Int31.
>
> I guess the easiest way to switch libraries is to have an NumbersSafe, 
> NumbersFast, NumbersOcaml and NumbersSimpl  folder with identical interfaces 
> and use the -Q option to map one of these to Numbers.  I will look into this 
> and do some experiments.
>
> If someone wants to review results from time to time, please let me know -  I 
> plan to publish this as extension to the standard library.
>
> Best regards,

That sounds really great.

For the NumberOcaml I guess if you are not really interested in modular 
arithmetic, you should just map it to an arbitary precision library.

--
Laurent