Stream: Coq users

Topic: Add auto hint per Lemma

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 ?

Paolo Giarrusso (Sep 22 2022 at 21:53):

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

Last updated: Oct 13 2024 at 01:02 UTC