Questions tagged [ocaml]
The ocaml tag has no usage guidance.
4 questions
1
vote
1
answer
59
views
Extracting Coq Lists to Lazy OCaml Lists?
When I use the following,
...
1
vote
1
answer
132
views
How do I work with ints when using coq-of-ocaml for OCaml to Coq conversion?
I am trying to use coq-of-ocaml to convert a simple recursive factorial function written in OCaml into Coq. I have a testing_factorial.ml file which defines the ...
6
votes
0
answers
92
views
What are Generic Arguments in Coq and how are they structured in their OCaml code?
I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
6
votes
0
answers
202
views
How does one systematically traverse OCaml representations of Coq ASTs terms?
I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language).
My main challenge is to figure out how to do this systematically because I ...