Apparently Hint Resolve
takes an optional pattern.
Can someone give me an example where the pattern is used (makes a difference)?
Do you want a real-world example or would an artificial one suffice?
The tiniest the better.
Here is one that loops if you don't specify the pattern:
Class mypred {A} (l : list A) := {}.
Lemma mypred_general {A} (l : list A) : @mypred A nil -> mypred l -> mypred l. Admitted.
#[local] Hint Resolve mypred_general | (mypred nil) : typeclass_instances.
Goal forall A (l : list A), mypred l. Fail apply _. Abort.
I guess you could use Timeout 1 Fail apply _
. With the pattern the search fails instantly so one second should be plenty even for CI.
OK, so it is relevant for typeclasses_eauto... I was trying calling trivial :-/
It seems that we can replace this line: https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssrnum.v#L1565
with Hint Resolve normr_ge0 | (is_true (0 <= norm _)) : core
. So it is orthogonal to type classes. Right?
It seems that we can replace this line
Only if the differences between ssr apply:
and Hint Resolve don't matter
We call trivial, what the game of apply:
?
Looking at the doc, anyway, I can't see where the pattern is used.
You can see the pattern in Print HintDb
It's the exact same kind of pattern as the one derived by Hint Resolve
without an explicit pattern. Not to be confused with the pattern of Hint Extern
which is printed the same way but behaves entirely different. (Hint Extern
patterns are matching purely syntactically, disregarding hint transparency.)
I see it, but I could not find a place where the manual explain when it is used, exactly.
Last updated: Oct 13 2024 at 01:02 UTC