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

Equations

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

partial def Lean.Elab.Structural.addSmartUnfoldingDefAux.visit (preDef : Lean.Elab.PreDefinition) (recArgPos : Nat) (e : Lean.Expr) : Lean.MetaM Lean.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 : Lean.Elab.PreDefinition) (recArgPos : Nat) : Lean.Elab.TermElabM Unit

Equations

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