Stream: Coq users

Topic: Add auto hint per Lemma

view this post on Zulip walker (Sep 22 2022 at 18:42):

Is it possible to add hints about certain theories to use in auto for just one lemma and then those hints will not apply for the rest of the coq file ?

view this post on Zulip Paolo Giarrusso (Sep 22 2022 at 21:53):

There are approximations: auto using lemma, or Local Hint Resolve inside a section

Last updated: Oct 03 2023 at 20:01 UTC