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

Indeed there is a PR open

https://github.com/coq/coq/pull/8252

Thanks! A very timely question I see :-)

The PR has been opened for 2 years though...

We've managed to convert our code to Int63 . How to extract those to ocaml? Is there a template available? @Maxime Dénès ?

Sorry found it:

https://coq.inria.fr/library/Coq.extraction.ExtrOCamlInt63.html

Last updated: Oct 13 2024 at 01:02 UTC