Disclaimer: trying to obtain efficient certified programs
by extracting
nat into
int is definitively *not* a good idea:
- Since int is bounded while nat is (theoretically) infinite,
you have to make sure by yourself that your program will not
manipulate numbers greater than
max_int. Otherwise you should
consider the translation of
nat into
big_int.
- Moreover, the mere translation of nat into int does not
change the complexity of functions. For instance,
mult stays
quadratic. To mitigate this, we propose here a few efficient (but
uncertified) realizers for some common functions over
nat.
This file is hence provided mainly for testing / prototyping
purpose. For serious use of numbers in extracted programs,
you are advised to use either coq advanced representations
(positive, Z, N, BigN, BigZ) or modular/axiomatic representation.