All Questions

Tagged with
Filter by
Sorted by
Tagged with
1 vote
1 answer
37 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 ...
5 votes
0 answers
53 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 ...
5 votes
0 answers
127 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 ...