structure Lean.Elab.WF.EqnInfoextends Lean.Elab.Eqns.EqnInfoCore : Type

• declName : Lake.Name
• levelParams : List Lake.Name
• type : Lean.Expr
• value : Lean.Expr
• declNames : Array Lake.Name
• declNameNonRec : Lake.Name
• fixedPrefixSize : Nat

instance Lean.Elab.WF.instInhabitedEqnInfo : Inhabited Lean.Elab.WF.EqnInfo

def Lean.Elab.WF.simpMatchWF? (info : Lean.Elab.WF.EqnInfo) (us : List Lean.Level) (fixedPrefix : Array Lean.Expr) (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Simplify match-expressions when trying to prove equation theorems for a recursive declaration defined using well-founded recursion. It is similar to simpMatch?, but is also tries to fold WellFounded.fix applications occurring in discriminants. See comment at tryToFoldWellFoundedFix.

def Lean.Elab.WF.simpMatchWF?.pre (info : Lean.Elab.WF.EqnInfo) (us : List Lean.Level) (fixedPrefix : Array Lean.Expr) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

def Lean.Elab.WF.mkEqns (declName : Lake.Name) (info : Lean.Elab.WF.EqnInfo) : Lean.MetaM (Array Lake.Name)

opaque Lean.Elab.WF.eqnInfoExt : Lean.MapDeclarationExtension Lean.Elab.WF.EqnInfo

def Lean.Elab.WF.registerEqnsInfo (preDefs : Array Lean.Elab.PreDefinition) (declNameNonRec : Lake.Name) (fixedPrefixSize : Nat) : Lean.MetaM Unit

def Lean.Elab.WF.getEqnsFor? (declName : Lake.Name) : Lean.MetaM (Option (Array Lake.Name))

def Lean.Elab.WF.getUnfoldFor? (declName : Lake.Name) : Lean.MetaM (Option Lake.Name)