The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928