def Lean.Meta.getInductiveUniverseAndParams (type : Lean.Expr) : Lean.MetaM (List Lean.Level × Array Lean.Expr)

Equations

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

def Lean.Meta.generalizeTargetsEq (mvarId : Lean.MVarId) (motiveType : Lean.Expr) (targets : Array Lean.Expr) : Lean.MetaM Lean.MVarId

Equations

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

structure Lean.Meta.GeneralizeIndicesSubgoal : Type

• mvarId : Lean.MVarId
• indicesFVarIds : Array Lean.FVarId
• fvarId : Lean.FVarId
• numEqs : Nat

def Lean.Meta.generalizeIndices (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM Lean.Meta.GeneralizeIndicesSubgoal

Similar to generalizeTargets but customized for the casesOn motive. Given a metavariable mvarId representing the

Ctx, h : I A j, D |- T

where fvarId is hs id, and the type I A j is an inductive datatype where A are parameters, and j the indices. Generate the goal

Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T

Remark: (j == j' -> h == h') is a "telescopic" equality. Remark: j is sequence of terms, and j' a sequence of free variables. The result contains the fields

• mvarId: the new goal
• indicesFVarIds: j' ids
• fvarId: h' id
• numEqs: number of equations in the target

structure Lean.Meta.CasesSubgoalextends Lean.Meta.InductionSubgoal : Type

• mvarId : Lean.MVarId
• fields : Array Lean.Expr
• subst : Lean.Meta.FVarSubst
• ctorName : Lean.Name

structure Lean.Meta.Cases.Context : Type

• inductiveVal : Lean.InductiveVal
• casesOnVal : Lean.DefinitionVal
• nminors : Nat
• majorDecl : Lean.LocalDecl
• majorTypeFn : Lean.Expr
• majorTypeArgs : Array Lean.Expr
• majorTypeIndices : Array Lean.Expr

partial def Lean.Meta.Cases.unifyEqs? (numEqs : Nat) (mvarId : Lean.MVarId) (subst : Lean.Meta.FVarSubst) (caseName? : Option Lean.Name := none) : Lean.MetaM (Option (Lean.MVarId × Lean.Meta.FVarSubst))

def Lean.Meta.Cases.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : Array Lean.Meta.AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) : Lean.MetaM (Array Lean.Meta.CasesSubgoal)

Equations

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

def Lean.MVarId.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : Array Lean.Meta.AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) : Lean.MetaM (Array Lean.Meta.CasesSubgoal)

Apply casesOn using the free variable majorFVarId as the major premise (aka discriminant). givenNames contains user-facing names for each alternative.

• useNatCasesAuxOn is a temporary hack for the rcases family of tactics. Do not use it, as it is subject to removal. It enables using Nat.casesAuxOn instead of Nat.casesOn, which causes case splits on n : Nat to be represented as 0 and n' + 1 rather than as Nat.zero and Nat.succ n'.

def Lean.MVarId.casesRec (mvarId : Lean.MVarId) (p : Lean.LocalDecl → Lean.MetaM Bool) : Lean.MetaM (List Lean.MVarId)

Keep applying cases on any hypothesis that satisfies p.

def Lean.MVarId.casesAnd (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Applies cases (recursively) to any hypothesis of the form h : p ∧ q.

Equations

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

def Lean.MVarId.substEqs (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Applies cases to any hypothesis of the form h : r = s.

Equations

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

structure Lean.Meta.ByCasesSubgoal : Type

Auxiliary structure for storing byCases tactic result.

• mvarId : Lean.MVarId
• fvarId : Lean.FVarId

def Lean.MVarId.byCases (mvarId : Lean.MVarId) (p : Lean.Expr) (hName : Lean.Name := `h) : Lean.MetaM (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal)

Split the goal in two subgoals: one containing the hypothesis h : p and another containing h : ¬ p.

def Lean.MVarId.byCasesDec (mvarId : Lean.MVarId) (p dec : Lean.Expr) (hName : Lean.Name := `h) : Lean.MetaM (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal)

Given dec : Decidable p, split the goal in two subgoals: one containing the hypothesis h : p and another containing h : ¬ p.

Equations

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