Lean.Meta.Match.CaseArraySizes

source

structure Lean.Meta.CaseArraySizesSubgoal :

Type

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

source

instance Lean.Meta.instInhabitedCaseArraySizesSubgoal :

Inhabited Lean.Meta.CaseArraySizesSubgoal

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.getArrayArgType a = do let aType ← Lean.Meta.inferType a let aType ← Lean.Meta.whnfD aType let _do_jp : PUnit → Lean.MetaM Lean.Expr := fun y => pure (Lean.Expr.appArg! aType) if Lean.Expr.isAppOfArity aType `Array 1 = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "array expected" ++ Lean.toMessageData (Lean.indentExpr a) ++ Lean.toMessageData "") _do_jp y

source

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)

Equations

Lean.Meta.caseArraySizes mvarId fvarId sizes xNamePrefix hNamePrefix = Lean.Meta.withMVarContext mvarId (let a := Lean.mkFVar fvarId; do let _ ← Lean.Meta.getArrayArgType a let aSize ← Lean.Meta.mkAppM `Array.size #[a] let mvarId ← Lean.Meta.assertExt mvarId `aSize (Lean.mkConst `Nat) aSize `h let discr ← Lean.Meta.intro1 mvarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (aSizeFVarId, mvarId) => do let discr ← Lean.Meta.intro1 mvarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (hEq, mvarId) => do let subgoals ← Lean.Meta.caseValues mvarId aSizeFVarId (Array.map Lean.mkRawNatLit sizes) hNamePrefix false Array.mapIdxM subgoals fun i subgoal => let subst := subgoal.subst; let mvarId := subgoal.mvarId; let hEqSz := Lean.Expr.fvarId! (Lean.Meta.FVarSubst.get subst hEq); if h : i.val < Array.size sizes then let n := Array.get sizes { val := i.val, isLt := h }; do let mvarId ← Lean.Meta.clear mvarId (Array.getOp subgoal.newHs 0) let mvarId ← Lean.Meta.clear mvarId (Lean.Expr.fvarId! (Lean.Meta.FVarSubst.get subst aSizeFVarId)) Lean.Meta.withMVarContext mvarId do let hEqSzSymm ← Lean.Meta.mkEqSymm (Lean.mkFVar hEqSz) let mvarId ← Lean.Meta.introArrayLit mvarId a n xNamePrefix hEqSzSymm let discr ← Lean.Meta.introN mvarId n [] false let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (xs, mvarId) => do let discr ← Lean.Meta.intro1 mvarId let x : Lean.FVarId × Lean.MVarId := discr match x with | (hEqLit, mvarId) => do let mvarId ← Lean.Meta.clear mvarId hEqSz let discr ← Lean.Meta.substCore mvarId hEqLit false subst true false let x : Lean.Meta.FVarSubst × Lean.MVarId := discr match x with | (subst, mvarId) => pure { mvarId := mvarId, elems := xs, diseqs := #[], subst := subst } else do let discr ← Lean.Meta.substCore mvarId hEq false subst true false let x : Lean.Meta.FVarSubst × Lean.MVarId := discr match x with | (subst, mvarId) => let diseqs := Array.map (fun fvarId => Lean.Expr.fvarId! (Lean.Meta.FVarSubst.get subst fvarId)) subgoal.newHs; pure { mvarId := mvarId, elems := #[], diseqs := diseqs, subst := subst })