Hi, For various reasons, I'm working on some code that traverses Coq's Constr.t
type.
I'd like to work out the type of arguments introduced by the bindings in each case of the Case constructor of the Constr.t
type.
For example:
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.
Ah, nice! Constr.expand_case
looks like exactly what I need. Thanks for the help!
Last updated: Dec 01 2023 at 06:01 UTC