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

• declName : Lean.Name
• levelParams : List Lean.Name
• type : Lean.Expr
• value : Lean.Expr
• recArgPos : Nat
• declNames : Array Lean.Name
• numFixed : Nat

instance Lean.Elab.Structural.instInhabitedEqnInfo : Inhabited Lean.Elab.Structural.EqnInfo

Equations

• Lean.Elab.Structural.instInhabitedEqnInfo = { default := { toEqnInfoCore := default, recArgPos := default, declNames := default, numFixed := default } }

def Lean.Elab.Structural.mkEqns (info : Lean.Elab.Structural.EqnInfo) : Lean.MetaM (Array Lean.Name)

Equations

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

opaque Lean.Elab.Structural.eqnInfoExt : Lean.MapDeclarationExtension Lean.Elab.Structural.EqnInfo

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

Equations

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

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

Equations

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

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

Equations

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

@[export lean_get_structural_rec_arg_pos]

def Lean.Elab.Structural.getStructuralRecArgPosImp? (declName : Lean.Name) : Lean.CoreM (Option Nat)

Equations

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