Hi there, I'm learning the Coq ocaml api and I'm stuck on a small issue. I have the name of a lemma (say Coq.Arith.Between.in_int_S
), and I want to turn it into a corresponding EConstr variable (say EConstr.mkVar (Names.Id.of_string the_name)
).
The issue is that it doesn't seem to handle the dots in the name : I get the error
Invalid character '.' in identifier "Coq.Arith.Between.in_int_S"
And if I use Names.Id.of_string_soft I get instead
Anomaly "in retyping: variable Coq.Arith.Between.in_int_S unbound."
I'm a bit lost in the different kinds of names used here, which function should I use ?
The function mkVar
is for section variables (or goal variables). If you have a global name, you should use mkConstU
instead.
If you are sure that the constant is not universe polymorphic, you can simply use UnsafeMonomorphic.mkConst
(where the UnsafeMonomorphic
precisely means "do it only if you are sure that the constant is not polymorphic").
Otherwise, if the constant is polymorphic or (virtually) polymorphic, depending on the situation you are, you may want:
fresh_constant_instance
, which automatically instantiates the universe variables with fresh universe parameters (e.g. if you are in the process of building a proof with a sigma
around)mkConstU (the_name, EConstr.EInstance (UVars.UContext.instance ctx))
if you are in some context of universe variable (e.g. if the_name
is a constant that occurs inside another polymorphic constant which itself depends on a universe context ctx
).Last updated: Oct 13 2024 at 01:02 UTC