Documentation

Lean.Elab.PreDefinition.Structural.SmartUnfolding

Auxiliary method for annotating match-alternatives with markSmartUnfoldingMatch and markSmartUnfoldingMatchAlt.

It uses the following approach:

  • Whenever it finds a match application e s.t. recArgHasLooseBVarsAt preDef.declName recArgPos e, it marks the match with markSmartUnfoldingMatch, and each alternative that does not contain a nested marked match is marked with markSmartUnfoldingMatchAlt.

Recall that the condition recArgHasLooseBVarsAt preDef.declName recArgPos e is the one used at mkBRecOn.