I'm trying to add multiple bi-implication hints like this to my hint database
Hint Resolve -> String.eqb_eq Nat.eqb_eq : reflection.
However, this fails because
eqb_eq_proj_l2r already exists.. It looks like the hint db is not using module names to disambiguate. How should I do this?
IIUC, you can use module names to disambiguate by hand. To export those hints to whoever imports this module:
Module Export String_extra. #[export] Hint Resolve -> String.eqb_eq : reflection. End String_extra. Module Export Nat_extra. #[export] Hint Resolve -> Nat.eqb_eq : reflection. End Nat_extra.
(You could also use
#[global] for the older semantics, but best use
#[export] and make sure to learn how it behaves).
Last updated: Sep 26 2023 at 11:01 UTC