source
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

Instances For

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

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

Instances For

source
instance Lean.Elab.PartialFixpoint.instInhabitedEqnInfo :
Inhabited EqnInfo
Equations

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

source
opaque Lean.Elab.PartialFixpoint.eqnInfoExt :
MapDeclarationExtension EqnInfo
source
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.

Instances For