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

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

Instances For

• Lean.Elab.WF.instInhabitedEqnInfo

instance Lean.Elab.WF.instInhabitedEqnInfo : Inhabited EqnInfo

Equations

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

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

Equations

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

opaque Lean.Elab.WF.eqnInfoExt : MapDeclarationExtension EqnInfo

def Lean.Elab.WF.registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) (argsPacker : Meta.ArgsPacker) (hasInduct : Bool) : MetaM Unit

Equations

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

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

Equations

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

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

Equations

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