Stream: Coq users

Topic: Add hint, name already exists

view this post on Zulip spaceloop (Jun 08 2021 at 16:24):

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?

view this post on Zulip Paolo Giarrusso (Jun 15 2021 at 04:41):

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: Oct 13 2024 at 01:02 UTC