structure Lean.Elab.Structural.EqnInfo : Type

• declName : Name
• levelParams : List Name
• type : Expr
• value : Expr
• recArgPos : Nat
• declNames : Array Name
• fixedParamPerms : FixedParamPerms

@[implicit_reducible]

instance Lean.Elab.Structural.instInhabitedEqnInfo : Inhabited EqnInfo

Equations

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

opaque Lean.Elab.Structural.eqnInfoExt : MapDeclarationExtension EqnInfo

def Lean.Elab.Structural.registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat) (fixedParamPerms : FixedParamPerms) : CoreM Unit

Equations

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