Documentation

Lean.Elab.PreDefinition.Structural.SmartUnfolding

Equations
• One or more equations did not get rendered due to their size.

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.

Equations
• One or more equations did not get rendered due to their size.