Documentation

Lean.Elab.PreDefinition.WF.Eqns

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

Type

declNames : Array Lean.Name
declNameNonRec : Lean.Name
fixedPrefixSize : Nat

instance Lean.Elab.WF.instInhabitedEqnInfo:

Inhabited Lean.Elab.WF.EqnInfo

Equations

Lean.Elab.WF.instInhabitedEqnInfo = { default := { toEqnInfoCore := default, declNames := default, declNameNonRec := default, fixedPrefixSize := default } }

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.

Equations

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

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

Equations

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

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

Lean.MetaM (Array Lean.Name)

Equations

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

opaque Lean.Elab.WF.eqnInfoExt:

Lean.MapDeclarationExtension Lean.Elab.WF.EqnInfo

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

Lean.CoreM Unit

Equations

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

def Lean.Elab.WF.getEqnsFor? (declName : Lean.Name) :

Lean.MetaM (Option (Array Lean.Name))

Equations

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

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

Lean.MetaM (Option Lean.Name)

Equations

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