structure Lean.Meta.CaseArraySizesSubgoal : Type

• mvarId : Lean.MVarId
• elems : Array Lean.FVarId
• diseqs : Array Lean.FVarId
• subst : Lean.Meta.FVarSubst

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

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

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

1. ..., 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.