Documentation

Lean.Elab.PreDefinition.Structural.SmartUnfolding

Equations
    Instances For

      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
        Instances For