To extract my program I'm using ExtrOcamlNatBigInt
.
However upon compilation I get errors such as:
File "coq/extract/Datatypes.mli", line 2, characters 25-36:
2 | val length : 'a1 list -> Big.big_int
^^^^^^^^^^^
Error: Unbound module Big
I'm not sure how to import module Big
; when I list it in the libraries
stanza in my dune file it doesn't know what Big
is.
How does one use ExtrOcamlNatBigInt
?
Thanks!
I think that module is supposed to extract to zarith
, tho you may need to include a copy of the big.ml file that lives in plugins/extraction
Emilio Jesús Gallego Arias said:
I think that module is supposed to extract to
zarith
, tho you may need to include a copy of the big.ml file that lives inplugins/extraction
Is there a way to import big.ml
or should I just create it and copy & paste the its contents?
I seems to recall that there was a bug open about it, I'd recommend just dropping the big.ml for now
other option would be to link the plugin, which seems to include it, but I don't recommend that, I'm checking Coq's bug tracker
You can see it is a really minimal wrapper
https://github.com/coq/coq/blob/master/plugins/extraction/big.ml
That's the relevant PR https://github.com/coq/coq/pull/8252
Last updated: Oct 13 2024 at 01:02 UTC