4 ms·
(* 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
by 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.