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