I’d like to reason about Coq code that will eventually be extracted to OCaml. As a result, I’d like to be able to write Coq code that can generate side-effect OCaml code that calls functions like
Digging through these papers for CoqOfOCaml (https://inria.hal.science/tel-01890983v1/document, https://v2.ocaml.org/meetings/ocaml/2014/ocaml2014_15.pdf), it seems like there is some library called “Pervasives” that can be used like this. However, looking at the repository, it doesn’t seem like this is the case anymore.
I’m thinking that I might be able to write an axiom like:
Axiom print_endline : string -> unit.
that would get lifted automatically to OCaml’s
print_endline. Am I on the right track, or is there a more elegant approach I can take?