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

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

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

Equations

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

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) (argsPacker : Lean.Meta.ArgsPacker) : Lean.MetaM 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))

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