Stream: Coq users

Topic: ✔ Recommended locality for type class Hint Mode

Karl Palmskog (Dec 21 2021 at 09:46):

Let's say I have a type class like the following:

Class Decision (P : Prop) := decide : {P} + {¬P}.
Hint Mode Decision ! : typeclass_instances.

Would the recommended hint locality always be #[global] for this case? Is there any situation one might want #[local] or #[export]?

Paolo Giarrusso (Dec 22 2021 at 00:04):

IIUC, you're declaring the clearly correct hint mode together with the typeclass at the outset, right? Then I'd recommend global, and very much not export.

Paolo Giarrusso (Dec 22 2021 at 00:06):

Also, under my assumptions, and assuming clients aren't hit by some bug, nobody is going to need to override the mode, so there's no use for export and local.

Paolo Giarrusso (Dec 22 2021 at 00:07):

However, all the assumptions I mentioned have exceptions.

Paolo Giarrusso (Dec 22 2021 at 00:10):

I recently git-committed a crime as follows (viewer discretion advised): Module danger. #[export] Hint Mode elem_of !!!!!! : kinda_core. Hint Resolve <lemma about elem_of that risks instantiating evars> : kinda_core. End danger.

Karl Palmskog (Dec 22 2021 at 08:39):

thanks, that's what I suspected

Notification Bot (Dec 22 2021 at 08:39):

Karl Palmskog has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC