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

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

instance Lean.Elab.Structural.instInhabitedEqnInfo : Inhabited EqnInfo

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

def Lean.Elab.Structural.mkEqns.doRealize (info : EqnInfo) (name : Name) (type : Expr) : MetaM Unit

opaque Lean.Elab.Structural.eqnInfoExt : MapDeclarationExtension EqnInfo

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

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

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

Generate the "unfold" lemma for declName.

def Lean.Elab.Structural.mkUnfoldEq.doRealize (declName : Name) (info : EqnInfo) (name : Name) : MetaM Unit

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

@[export lean_get_structural_rec_arg_pos]

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