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

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

Instances For

• Lean.Elab.Structural.instInhabitedEqnInfo

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 Lake.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 Lake.Name) (recArgPos : Nat) (numFixed : Nat) : Lean.CoreM Unit

Equations

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

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

Equations

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

def Lean.Elab.Structural.getUnfoldFor? (declName : Lake.Name) : Lean.MetaM (Option Lake.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 : Lake.Name) : Lean.CoreM (Option Nat)

Equations

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