Improve description of grind_pattern #640
Description
What question should the reference manual answer?
This feedback was provided on Zulip:
I'm finally getting around to reading about grind in the reference manual. In 17.6.1 the introduction of grind_pattern gf => f x is done in a sort of matter-of-fact way, but its not clear (a) what exactly that does, or (b) why that suddenly causes grind to be able to solve the goal. The lead up to that motivates the move by explaining that the base gf rule doesn't fire (at least in part) because "the goal does not even contain the function symbol g", but the goal doesn't contain f either.