Lean.Meta.Tactic.Cases

source

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.

source

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.

source

structure Lean.Meta.GeneralizeIndicesSubgoal:

Type

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

source

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

Equations

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

source

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

Type

ctorName : Lean.Name

source

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

source

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

Lean.MetaM (Option (Lean.MVarId × Lean.Meta.FVarSubst))

source

def Lean.Meta.Cases.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) :

Lean.MetaM (Array Lean.Meta.CasesSubgoal)

Equations

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

source

def Lean.Meta.cases (mvarId : Lean.MVarId) (majorFVarId : Lean.FVarId) (givenNames : optParam (Array Lean.Meta.AltVarNames) #[]) :

Lean.MetaM (Array Lean.Meta.CasesSubgoal)

Equations

Lean.Meta.cases mvarId majorFVarId givenNames = Lean.Meta.Cases.cases mvarId majorFVarId givenNames

source

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

Lean.MetaM (List Lean.MVarId)

Equations

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

source

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

Lean.MetaM Lean.MVarId

Equations

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

source

def Lean.Meta.substEqs (mvarId : Lean.MVarId) :

Lean.MetaM (Option Lean.MVarId)

Equations

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

source

structure Lean.Meta.ByCasesSubgoal:

Type

mvarId : Lean.MVarId
fvarId : Lean.FVarId

source

def Lean.Meta.byCases (mvarId : Lean.MVarId) (p : Lean.Expr) (hName : optParam Lean.Name `h) :

Lean.MetaM (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal)

Equations

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

source

def Lean.Meta.byCases.toByCasesSubgoal (s : Lean.Meta.CasesSubgoal) :

Lean.MetaM Lean.Meta.ByCasesSubgoal

Equations

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