structure Lean.Elab.PartialFixpoint.EqnInfo : Type

• declName : Name
• levelParams : List Name
• type : Expr
• value : Expr
• declNames : Array Name
• declNameNonRec : Name
• fixedParamPerms : FixedParamPerms
• fixpointType : Array PartialFixpointType

def Lean.Elab.PartialFixpoint.instInhabitedEqnInfo.default : EqnInfo

instance Lean.Elab.PartialFixpoint.instInhabitedEqnInfo : Inhabited EqnInfo

opaque Lean.Elab.PartialFixpoint.eqnInfoExt : MapDeclarationExtension EqnInfo

def Lean.Elab.PartialFixpoint.registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms) (fixpointType : Array PartialFixpointType) : MetaM Unit