def Lean.Elab.Structural.addSmartUnfoldingDefAux (preDef : PreDefinition) (recArgPos : Nat) : MetaM PreDefinition

Equations

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

partial def Lean.Elab.Structural.addSmartUnfoldingDefAux.visit (preDef : PreDefinition) (recArgPos : Nat) (e : Expr) : MetaM Expr

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.

def Lean.Elab.Structural.addSmartUnfoldingDef (preDef : PreDefinition) (recArgPos : Nat) : TermElabM Unit

Equations

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