Documentation

Lean.Meta.Match.CaseArraySizes

structure Lean.Meta.CaseArraySizesSubgoal:

Type

instance Lean.Meta.instInhabitedCaseArraySizesSubgoal:

Inhabited Lean.Meta.CaseArraySizesSubgoal

Equations

Lean.Meta.instInhabitedCaseArraySizesSubgoal = { default := { mvarId := default, elems := default, diseqs := default, subst := default } }

def Lean.Meta.getArrayArgType (a : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

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

def Lean.Meta.caseArraySizes (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (sizes : Array Nat) (xNamePrefix : optParam Lean.Name `x) (hNamePrefix : optParam Lean.Name `h) :

Lean.MetaM (Array Lean.Meta.CaseArraySizesSubgoal)

Split goal ... |- C a into sizes.size + 1 subgoals

..., x_1 ... x_{sizes[0]} |- C #[x_1, ... x_{sizes[0]}] ... n) ..., x_1 ... x_{sizes[n-1]} |- C #[x_1, ..., x_{sizes[n-1]}] n+1) ..., (h_1 : a.size != sizes[0]), ..., (h_n : a.size != sizes[n-1]) |- C a where n = sizes.size

Equations

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