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

• declName : Name
• levelParams : List Name
• type : Expr
• value : Expr
• declNames : Array Name
• declNameNonRec : Name
• argsPacker : Meta.ArgsPacker
• fixedParamPerms : FixedParamPerms

instance Lean.Elab.WF.instInhabitedEqnInfo : Inhabited EqnInfo

Equations

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

opaque Lean.Elab.WF.eqnInfoExt : MapDeclarationExtension EqnInfo

def Lean.Elab.WF.registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) : 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.copyPrivateUnfoldTheorem : Meta.GetUnfoldEqnFn

This is a hack to fix fallout from #8519, where a non-exposed wfrec definition foo in a module would cause foo.eq_def to be defined eagerly and privately, but it should still be visible from non-mudule files.

So we create a unfold equation generator that aliases an existing private eq_def to wherever the current module expects it.

Equations

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