Documentation

Lean.Elab.PreDefinition.Structural.SmartUnfolding

source
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.
source
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`.
source
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.