Bas Spitters (Sep 08 2020 at 16:41): Bas Spitters (Sep 08 2020 at 16:41):I understand that ocaml moved to zarith and away from num
https://github.com/ocaml/num
https://github.com/ocaml/Zarith
However, these still seem to extract to num:
https://coq.inria.fr/distrib/current/stdlib//Coq.extraction.ExtrOcamlZBigInt.html
Is my understanding correct? Does anyone have a translation to Zarith laying around?
List of Extraction layers:
https://coq.inria.fr/library/index_global_E.html
Emilio Jesús Gallego Arias (Sep 08 2020 at 16:41):Indeed there is a PR open
Emilio Jesús Gallego Arias (Sep 08 2020 at 16:42):https://github.com/coq/coq/pull/8252
Bas Spitters (Sep 08 2020 at 16:56):Thanks! A very timely question I see :-)
Théo Zimmermann (Sep 08 2020 at 17:12):The PR has been opened for 2 years though...
Bas Spitters (Sep 09 2020 at 11:52):We've managed to convert our code to Int63 . How to extract those to ocaml? Is there a template available? @Maxime Dénès ?
Bas Spitters (Sep 09 2020 at 11:52):Sorry found it:
https://coq.inria.fr/library/Coq.extraction.ExtrOCamlInt63.html
Last updated: Jun 01 2023 at 11:01 UTC