4 ms·
Why not use a binary number representation? They are in the library: https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNat.htm https://coq.inria.fr/dis
by sddfd 9y ago
Why not use a binary number representation?
They are in the library:
https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNat.htm https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNa...
If you use Z, even the Omega tactic (solver for presburger arithmetic) should work.
- MichaelBurge 9y ago(* edit: profquail below points out that the Integer variant of the Z extraction module has a less strongly-worded disclaimer. Just importing it would probably fix the described memory issue. *) https://github.com/coq/coq/blob/307f08d2ad2aca5d48441394342af4615810d0c7/plugins/extraction/ExtrHaskellZInteger.v https://github.com/coq/coq/blob/307f08d2ad2aca5d48441394342a...
- profquail 9y agoCan it extract [Z] to some bigint implementation based on gmp? That should still be safe but provide better performance than using Peano arithmetic.