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

Information about an eliminator as used by induction or cases.

Created from an expression by getElimInfo. This typically contains level metavariables that are instantiated as we go (e.g. in addImplicitTargets), so this is single use.

• elimExpr : Lean.Expr
• elimType : Lean.Expr
• 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 := { elimExpr := default, elimType := default, motivePos := default, targetsPos := default, altsInfo := default } }

def Lean.Meta.getElimExprInfo (elimExpr : Lean.Expr) (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.getElimInfo (elimName : Lake.Name) (baseDeclName? : optParam (Option Lake.Name) none) : Lean.MetaM Lean.Meta.ElimInfo

Equations

• Lean.Meta.getElimInfo elimName baseDeclName? = do let __do_lift ← Lean.Meta.mkConstWithFreshMVarLevels elimName Lean.Meta.getElimExprInfo __do_lift baseDeclName?

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) (implicits : Array Lean.MVarId) (targets' : Array Lean.Expr) : Lean.MetaM (Array Lean.MVarId × Array Lean.Expr)

structure Lean.Meta.CustomEliminator : Type

• typeNames : Array Lake.Name
• elimName : Lake.Name

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

Equations

• Lean.Meta.instInhabitedCustomEliminator = { default := { typeNames := default, elimName := 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) Lake.Name

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.elimName }

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

def Lean.Meta.mkCustomEliminator (elimName : 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 Lake.Name)

Equations

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