Stream: Coq devs & plugin devs

Topic: Creating an EConstr variable


view this post on Zulip Mathis Bouverot-Dupuis (Apr 09 2024 at 14:52):

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 ?

view this post on Zulip Hugo Herbelin (Apr 09 2024 at 16:03):

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:


Last updated: Oct 13 2024 at 01:02 UTC