Hello, I have some problems about adding hints to hint databases. For example, the following code:
Theorem lem1 : forall x y : nat, x + y = y + x.
Proof.
...
Qed.
Theorem goal : forall x y : nat, x + y = y + x.
Proof.
my_tactic.
...
Qed.
my_tactic
is the tactic that I implement by Coq API. In my_tactic
, I want to implement this functionality by using the Coq API, similar to what the following Coq code achieves:
Create HintDb newdb.
Hint Resolve lem1:newdb.
Now, I could use Hints.create_hint_db
to create a new hint database, and I see Hints.add_hints : locality:hint_locality -> hint_db_name list -> hints_entry -> unit
may be able to add hints to the hint database. But I do not know how to get lem1
from environment and use it to create the hints_entry
structure. Is there some ways to achieve it or other ways to add lem1
to the new hint database?
By the way, I'm very interested in Coq internals. When I encounter APIs that I don't understand, I read the source code to understand them. However, sometimes I could not understand what some parts of the code does and why it should be done this way. Are there any documents about coq internals that could recommend?
Last updated: Oct 13 2024 at 01:02 UTC