structure Lean.Meta.ElimAltInfo : Type

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

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

Equations

• Lean.Meta.instReprElimAltInfo = { reprPrec := Lean.Meta.reprElimAltInfo✝ }

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

Equations

• Lean.Meta.instInhabitedElimAltInfo = { default := { name := default, declName? := default, numFields := default } }

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

Equations

• Lean.Meta.instReprElimInfo = { reprPrec := Lean.Meta.reprElimInfo✝ }

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

Equations

• Lean.Meta.instInhabitedElimInfo = { default := { name := default, motivePos := default, targetsPos := default, altsInfo := default } }

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

Equations

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

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.

Equations

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

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

Equations

• Lean.Meta.instInhabitedCustomEliminator = { default := { typeNames := default, elimInfo := default } }

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

Equations

• Lean.Meta.instReprCustomEliminator = { reprPrec := Lean.Meta.reprCustomEliminator✝ }

structure Lean.Meta.CustomEliminators : Type

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

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

Equations

• Lean.Meta.instInhabitedCustomEliminators = { default := { map := default } }

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

Equations

• Lean.Meta.instReprCustomEliminators = { reprPrec := Lean.Meta.reprCustomEliminators✝ }

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

Equations

• Lean.Meta.addCustomEliminatorEntry es e = match es with | { map := map } => { map := Lean.SMap.insert map e.typeNames e.elimInfo }

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

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

Equations

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

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

Equations

• Lean.Meta.addCustomEliminator declName attrKind = do let e ← Lean.Meta.mkCustomEliminator declName Lean.ScopedEnvExtension.add Lean.Meta.customEliminatorExt e attrKind

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

Equations

• Lean.Meta.getCustomEliminators = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.customEliminatorExt __do_lift)

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

Equations

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