Stream: Coq users

Topic: ✔ Recommended locality for type class Hint Mode


view this post on Zulip 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]?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 22 2021 at 00:07):

However, all the assumptions I mentioned have exceptions.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Dec 22 2021 at 08:39):

thanks, that's what I suspected

view this post on Zulip Notification Bot (Dec 22 2021 at 08:39):

Karl Palmskog has marked this topic as resolved.


Last updated: Mar 28 2024 at 21:01 UTC