General grind/simp annotation guidance

Stream: new members

[cmlsharp]

Are there any codified heuristics about what types of theorems should be given grind annotations? E.g. are there cases where a lemma should have a @[simp] annotation, but not some kind of @[grind ?] annotation?