unfold modifyM
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
⊢ SatisfiesM (fun y => size y = size x) (modifyM x n f)
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)