Hi, For various reasons, I'm working on some code that traverses Coq's
I'd like to work out the type of arguments introduced by the bindings in each case of the Case constructor of the
match Constr.kind c with ... | Constr.Case (info, _univ, _ty, _ret, _inv, _vl, cases) -> ...
By iterating through the
cases binding above, I can obtain the subterms within a given proof term by looking at the second component of each element in
cases. The first component seems to tell me the variables that are bound by case, but don't include the types of these variables.
Could someone point me to any of the Coq API's I could use to retrieve this information?
Okay, after digging around, I figure the right direction to go is something like:
let mind = Environ.lookup_mind (fst info.ci_ind) coq_env in (* do something with mind.mind_packets *)
Is this the correct approach, or is there something simpler?
For EConstr, there is a function
EConstr.annotate_case that does this. Otherwise you can either do it by hand using the same kind of code, or destruct the branches generated by
Constr.expand_case with number of declarations given by the names.
Constr.expand_case looks like exactly what I need. Thanks for the help!
Last updated: Dec 01 2023 at 06:01 UTC