Skip to main content

Questions tagged [ocaml]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1 vote
1 answer
59 views

Extracting Coq Lists to Lazy OCaml Lists?

When I use the following, ...
Agnishom Chattopadhyay's user avatar
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 ...
bodacious_bandit's user avatar
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 ...
Charlie Parker's user avatar
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 ...
Charlie Parker's user avatar