structure Lean.Meta.ElimAltInfo : Type

• name : Name
• declName? : Option Name

  A declaration corresponding to the inductive constructor. (For custom recursors, the alternatives correspond to parameter names in the recursor, so we may not have a declaration to point to.) This is used for go-to-definition on the alternative name.

• numFields : Nat
• provesMotive : Bool

  If provesMotive := true, then this alternative has motive as its conclusion. Only for those alternatives the induction tactic should introduce reverted hypotheses.

instance Lean.Meta.instReprElimAltInfo : Repr ElimAltInfo

Equations

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

instance Lean.Meta.instInhabitedElimAltInfo : Inhabited ElimAltInfo

Equations

• Lean.Meta.instInhabitedElimAltInfo = { default := { name := default, declName? := default, numFields := default, provesMotive := 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 : Expr
• elimType : Expr
• motivePos : Nat
• targetsPos : Array Nat
• altsInfo : Array ElimAltInfo
• numComplexMotiveArgs : Nat

  Extra arguments to the motive, after the targets, that are instantiated with non-atomic expressions in the goal

instance Lean.Meta.instReprElimInfo : Repr ElimInfo

Equations

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

instance Lean.Meta.instInhabitedElimInfo : Inhabited ElimInfo

Equations

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

def Lean.Meta.altArity (motive : Expr) (n : Nat) : Expr → Nat × Bool

Given the type t of an alternative, determines the number of parameters (.forall and .let)-bound, and whether the conclusion is a motive-application.

Equations

• Lean.Meta.altArity motive n (Lean.Expr.forallE binderName binderType b binderInfo) = Lean.Meta.altArity motive (n + 1) b
• Lean.Meta.altArity motive n (Lean.Expr.letE declName type value b nonDep) = Lean.Meta.altArity motive (n + 1) b
• Lean.Meta.altArity motive n x✝ = (n, x✝.getAppFn == motive)

def Lean.Meta.getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : MetaM ElimInfo

Equations

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

def Lean.Meta.getElimInfo (elimName : Name) (baseDeclName? : Option Name := none) : MetaM 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 : ElimInfo) (targets : Array Expr) : MetaM (Array 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 : ElimInfo) (targets : Array Expr) (type : Expr) (argIdx targetIdx : Nat) (implicits : Array MVarId) (targets' : Array Expr) : MetaM (Array MVarId × Array Expr)

structure Lean.Meta.CustomEliminator : Type

• induction : Bool
• typeNames : Array Name
• elimName : Name

instance Lean.Meta.instInhabitedCustomEliminator : Inhabited CustomEliminator

Equations

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

instance Lean.Meta.instReprCustomEliminator : Repr CustomEliminator

Equations

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

structure Lean.Meta.CustomEliminators : Type

• map : SMap (Bool × Array Name) Name

instance Lean.Meta.instInhabitedCustomEliminators : Inhabited CustomEliminators

Equations

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

instance Lean.Meta.instReprCustomEliminators : Repr CustomEliminators

Equations

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

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

Equations

• Lean.Meta.addCustomEliminatorEntry { map := map } e = { map := map.insert (e.induction, e.typeNames) e.elimName }

opaque Lean.Meta.customEliminatorExt : SimpleScopedEnvExtension CustomEliminator CustomEliminators

def Lean.Meta.mkCustomEliminator (elimName : Name) (induction : Bool) : MetaM CustomEliminator

Equations

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

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

Equations

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

def Lean.Meta.getCustomEliminators : CoreM CustomEliminators

Gets all the eliminators defined using the @[induction_eliminator] and @[cases_eliminator] attributes.

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 Expr) (induction : Bool) : MetaM (Option Name)

Gets an eliminator appropriate for the provided array of targets. If induction is true then returns a matching eliminator defined using the @[induction_eliminator] attribute and otherwise returns one defined using the @[cases_eliminator] attribute.

The @[induction_eliminator] attribute is for the induction tactic and the @[cases_eliminator] attribute is for the cases tactic.

Equations

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