structure Lean.Meta.CaseArraySizesSubgoal : Type

• mvarId : MVarId
• elems : Array FVarId
• diseqs : Array FVarId
• subst : FVarSubst

@[instance_reducible]

instance Lean.Meta.instInhabitedCaseArraySizesSubgoal : Inhabited CaseArraySizesSubgoal

Equations

• Lean.Meta.instInhabitedCaseArraySizesSubgoal = { default := Lean.Meta.instInhabitedCaseArraySizesSubgoal.default }

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

Equations

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

def Lean.Meta.caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix : Name := `x) (hNamePrefix : Name := `h) : MetaM (Array 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.