5.6. Restricting e-matching in a grind call🔗

If instead of modifying how lemmas are tagged, you want to limit e-matching in your grind call, you can for example do this by restricting "generations". Each expression on the whiteboard has a associated generation. The expressions from the original context all have generation 0. When we produce a new expression through e-matching, its generation will be one higher than that of the term with the highest generation that was used for producing the new expression.

You can write grind (gen := n) to modify how low the generation number needs to be for e-matching to consider a term. The default is 8.