structure Lean.Elab.PartialFixpoint.EqnInfoextends Lean.Elab.Eqns.EqnInfoCore : 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

Equations

• Lean.Elab.PartialFixpoint.instInhabitedEqnInfo.default = { toEqnInfoCore := default, declNames := default, declNameNonRec := default, fixedParamPerms := default, fixpointType := default }

instance Lean.Elab.PartialFixpoint.instInhabitedEqnInfo : Inhabited EqnInfo

Equations

• Lean.Elab.PartialFixpoint.instInhabitedEqnInfo = { default := Lean.Elab.PartialFixpoint.instInhabitedEqnInfo.default }

opaque Lean.Elab.PartialFixpoint.eqnInfoExt : MapDeclarationExtension EqnInfo

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

Equations

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

partial def Lean.Elab.PartialFixpoint.rwFixUnder (lhs : Expr) : MetaM Expr

def Lean.Elab.PartialFixpoint.mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name

Generate the "unfold" lemma for declName.

Equations

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

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

Equations

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

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

Equations

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