structure Lean.Meta.ElimAltInfo : Type

• name : Lake.Name
• declName? : Option Lake.Name
• numFields : Nat

instance Lean.Meta.instReprElimAltInfo : Repr Lean.Meta.ElimAltInfo

instance Lean.Meta.instInhabitedElimAltInfo : Inhabited Lean.Meta.ElimAltInfo

structure Lean.Meta.ElimInfo : Type

• name : Lake.Name
• motivePos : Nat
• targetsPos : Array Nat
• altsInfo : Array Lean.Meta.ElimAltInfo

instance Lean.Meta.instReprElimInfo : Repr Lean.Meta.ElimInfo

instance Lean.Meta.instInhabitedElimInfo : Inhabited Lean.Meta.ElimInfo

def Lean.Meta.getElimInfo (declName : Lake.Name) (baseDeclName? : optParam (Option Lake.Name) none) : Lean.MetaM Lean.Meta.ElimInfo

def Lean.Meta.addImplicitTargets (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) : Lean.MetaM (Array Lean.Expr)

Eliminators/recursors may have implicit targets. For builtin recursors, all indices are implicit targets. Given an eliminator and the sequence of explicit targets, this methods returns a new sequence containing implicit and explicit targets.

partial def Lean.Meta.addImplicitTargets.collect (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr) (type : Lean.Expr) (argIdx : Nat) (targetIdx : Nat) (targets' : Array Lean.Expr) : Lean.MetaM (Array Lean.Expr)

structure Lean.Meta.CustomEliminator : Type

• typeNames : Array Lake.Name
• elimInfo : Lean.Meta.ElimInfo

instance Lean.Meta.instInhabitedCustomEliminator : Inhabited Lean.Meta.CustomEliminator

instance Lean.Meta.instReprCustomEliminator : Repr Lean.Meta.CustomEliminator

structure Lean.Meta.CustomEliminators : Type

• map : Lean.SMap (Array Lake.Name) Lean.Meta.ElimInfo

instance Lean.Meta.instInhabitedCustomEliminators : Inhabited Lean.Meta.CustomEliminators

instance Lean.Meta.instReprCustomEliminators : Repr Lean.Meta.CustomEliminators

def Lean.Meta.addCustomEliminatorEntry (es : Lean.Meta.CustomEliminators) (e : Lean.Meta.CustomEliminator) : Lean.Meta.CustomEliminators

opaque Lean.Meta.customEliminatorExt : Lean.SimpleScopedEnvExtension Lean.Meta.CustomEliminator Lean.Meta.CustomEliminators

def Lean.Meta.mkCustomEliminator (declName : Lake.Name) : Lean.MetaM Lean.Meta.CustomEliminator

def Lean.Meta.addCustomEliminator (declName : Lake.Name) (attrKind : Lean.AttributeKind) : Lean.MetaM Unit

def Lean.Meta.getCustomEliminators : Lean.CoreM Lean.Meta.CustomEliminators

def Lean.Meta.getCustomEliminator? (targets : Array Lean.Expr) : Lean.MetaM (Option Lean.Meta.ElimInfo)