Good practices for grind

Stream: new members

[Juanjo Madrigal]

Hi!

I'd like to ask an "open-ended question" about good practices in the use of the tactic grind.

I'm currently learning Lean by trying to implement the contents of a book and I'm finding that grind is extremely powerful, so many of the last advances are full of <;> grind and @[grind] all over the place (e.g. here).

But I guess that in the long term it may be dangerous to abuse of it, perhaps due to performance or legibility or other reasons. I would like to know if there are some heuristics, rules of thumbs, or advice, in some thread or document, about a use of grind/simp to be considered correct in a good quality code. Or perhaps it is always preferred to have shorter code at any price?

Thank you!!

[Kenny Lau]

In my experience (and in the official post) I think grind is designed to be quite efficient, and usually faster than say aesop and ring

[Juanjo Madrigal]

Thank you @Kenny Lau !! So there seems to be no problem in using grind "as much as possible" :raised_hands: