From fdab3b90b9ad402a91d2191b6bb80231900e6c6e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Oct 2019 16:46:05 -0700
Subject: [PATCH] refactor(library/init/data/array): new name convention for
 Array functions

---
 library/init/data/array/basic.lean            | 102 +++++++++---------
 library/init/data/array/binsearch.lean        |   2 +-
 library/init/data/array/qsort.lean            |  14 +--
 library/init/data/bytearray/basic.lean        |  10 +-
 library/init/data/hashmap/basic.lean          |   4 +-
 library/init/data/persistentarray/basic.lean  |  22 ++--
 .../init/data/persistenthashmap/basic.lean    |  40 +++----
 library/init/lean/attributes.lean             |   2 +-
 library/init/lean/compiler/externattr.lean    |  12 +--
 library/init/lean/compiler/ir/basic.lean      |   2 +-
 library/init/lean/compiler/ir/borrow.lean     |   8 +-
 library/init/lean/compiler/ir/boxing.lean     |   6 +-
 library/init/lean/compiler/ir/emitc.lean      |  36 +++----
 .../lean/compiler/ir/expandresetreuse.lean    |   8 +-
 library/init/lean/compiler/ir/pushproj.lean   |   2 +-
 library/init/lean/compiler/ir/rc.lean         |  16 +--
 library/init/lean/compiler/ir/simpcase.lean   |   8 +-
 library/init/lean/elaborator/preterm.lean     |   4 +-
 library/init/lean/environment.lean            |  20 ++--
 library/init/lean/localcontext.lean           |   2 +-
 library/init/lean/parser/parser.lean          |   2 +-
 library/init/lean/parser/transform.lean       |   4 +-
 library/init/lean/position.lean               |   8 +-
 library/init/lean/syntax.lean                 |  18 ++--
 tests/bench/qsort.lean                        |  16 +--
 tests/bench/unionfind.lean                    |  12 +--
 tests/compiler/bytearray_bug.lean             |   2 +-
 tests/compiler/phashmap.lean                  |   6 +-
 tests/compiler/phashmap2.lean                 |   6 +-
 tests/compiler/phashmap3.lean                 |   6 +-
 tests/lean/bytearray.lean                     |   4 +-
 tests/lean/ref1.lean                          |   2 +-
 tests/lean/repr_issue.lean                    |   4 +-
 33 files changed, 207 insertions(+), 203 deletions(-)

diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 7cdd500512..efc7d9120d 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -65,7 +65,7 @@ def singleton (v : α) : Array α :=
 mkArray 1 v
 
 @[extern c inline "lean_array_fget(#2, #3)"]
-def fget (a : @& Array α) (i : @& Fin a.size) : α :=
+def get (a : @& Array α) (i : @& Fin a.size) : α :=
 a.data i
 
 /- Low-level version of `fget` which is as fast as a C array read.
@@ -73,25 +73,25 @@ a.data i
    `fget` may be slightly slower than `uget`. -/
 @[extern c inline "lean_array_uget(#2, #3)"]
 def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
-a.fget ⟨i.toNat, h⟩
+a.get ⟨i.toNat, h⟩
 
 /- "Comfortable" version of `fget`. It performs a bound check at runtime. -/
 @[extern c inline "lean_array_get(#2, #3, #4)"]
-def get [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
-if h : i < a.size then a.fget ⟨i, h⟩ else default α
+def get! [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
+if h : i < a.size then a.get ⟨i, h⟩ else default α
 
 def back [Inhabited α] (a : Array α) : α :=
-a.get (a.size - 1)
+a.get! (a.size - 1)
 
-def getOpt (a : Array α) (i : Nat) : Option α :=
-if h : i < a.size then some (a.fget ⟨i, h⟩) else none
+def get? (a : Array α) (i : Nat) : Option α :=
+if h : i < a.size then some (a.get ⟨i, h⟩) else none
 
 @[extern c inline "lean_array_fset(#2, #3, #4)"]
-def fset (a : Array α) (i : @& Fin a.size) (v : α) : Array α :=
+def set (a : Array α) (i : @& Fin a.size) (v : α) : Array α :=
 { sz   := a.sz,
   data := fun j => if h : i = j then v else a.data j }
 
-theorem szFSetEq (a : Array α) (i : Fin a.size) (v : α) : (fset a i v).size = a.size :=
+theorem szFSetEq (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
 rfl
 
 theorem szPushEq (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
@@ -102,39 +102,43 @@ rfl
    `fset` may be slightly slower than `uset`. -/
 @[extern c inline "lean_array_uset(#2, #3, #4)"]
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
-a.fset ⟨i.toNat, h⟩ v
+a.set ⟨i.toNat, h⟩ v
 
 /- "Comfortable" version of `fset`. It performs a bound check at runtime. -/
 @[extern c inline "lean_array_set(#2, #3, #4)"]
-def set (a : Array α) (i : @& Nat) (v : α) : Array α :=
-if h : i < a.size then a.fset ⟨i, h⟩ v else a
+def set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
+if h : i < a.size then a.set ⟨i, h⟩ v else panic! "index out of bounds"
 
 @[extern c inline "lean_array_fswap(#2, #3, #4)"]
-def fswap (a : Array α) (i j : @& Fin a.size) : Array α :=
-let v₁ := a.fget i;
-let v₂ := a.fget j;
-let a  := a.fset i v₂;
-a.fset j v₁
+def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
+let v₁ := a.get i;
+let v₂ := a.get j;
+let a  := a.set i v₂;
+a.set j v₁
 
 @[extern c inline "lean_array_swap(#2, #3, #4)"]
-def swap (a : Array α) (i j : @& Nat) : Array α :=
+def swap! (a : Array α) (i j : @& Nat) : Array α :=
 if h₁ : i < a.size then
-if h₂ : j < a.size then fswap a ⟨i, h₁⟩ ⟨j, h₂⟩
-else a
-else a
+if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩
+else panic! "index out of bounds"
+else panic! "index out of bounds"
 
-@[inline] def fswapAt {α : Type} (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
-let e := a.fget i;
-let a := a.fset i v;
+@[inline] def swapAt {α : Type} (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
+let e := a.get i;
+let a := a.set i v;
 (e, a)
 
-@[inline] def swapAt {α : Type} (a : Array α) (i : Nat) (v : α) : α × Array α :=
-if h : i < a.size then fswapAt a ⟨i, h⟩ v else (v, a)
+-- TODO: delete as soon as we can define local instances
+@[neverExtract] private def swapAtPanic! [Inhabited α] (i : Nat) : α × Array α :=
+panic! ("index " ++ toString i ++ " out of bounds")
+
+@[inline] def swapAt! {α : Type} (a : Array α) (i : Nat) (v : α) : α × Array α :=
+if h : i < a.size then swapAt a ⟨i, h⟩ v else @swapAtPanic! _ ⟨v⟩ i
 
 @[extern c inline "lean_array_pop(#2)"]
 def pop (a : Array α) : Array α :=
 { sz   := Nat.pred a.size,
-  data := fun ⟨j, h⟩ => a.fget ⟨j, Nat.ltOfLtOfLe h (Nat.predLe _)⟩ }
+  data := fun ⟨j, h⟩ => a.get ⟨j, Nat.ltOfLtOfLe h (Nat.predLe _)⟩ }
 
 -- TODO(Leo): justify termination using wf-rec
 partial def shrink : Array α → Nat → Array α
@@ -149,7 +153,7 @@ variables {β : Type v} {σ : Type u}
 | i, b =>
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩;
-     f idx (a.fget idx) b >>= miterateAux (i+1)
+     f idx (a.get idx) b >>= miterateAux (i+1)
   else pure b
 
 @[inline] def miterate (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → m β) : m β :=
@@ -168,7 +172,7 @@ miterateAux a (fun _ b a => f a b) ini b
      let idx₁ : Fin a₁.size := ⟨i, h₁⟩;
      if h₂ : i < a₂.size then
        let idx₂ : Fin a₂.size := ⟨i, h₂⟩;
-       f idx₁ (a₁.fget idx₁) (a₂.fget idx₂) b >>= miterate₂Aux (i+1)
+       f idx₁ (a₁.get idx₁) (a₂.get idx₂) b >>= miterate₂Aux (i+1)
      else pure b
   else pure b
 
@@ -184,7 +188,7 @@ miterate₂ a₁ a₂ b (fun _ a₁ a₂ b => f b a₁ a₂)
 | i =>
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩;
-     do r ← f (a.fget idx);
+     do r ← f (a.get idx);
         match r with
         | some v => pure r
         | none   => mfindAux (i+1)
@@ -200,7 +204,7 @@ mfindAux a f 0
     have i - 1 < a.size from Nat.ltOfLtOfLe this h;
     let idx : Fin a.size := ⟨i - 1, this⟩;
     do
-      r ← f (a.fget idx);
+      r ← f (a.get idx);
       match r with
       | some v => pure r
       | none   =>
@@ -248,7 +252,7 @@ variables {m : Type → Type w} [Monad m]
 | i =>
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩;
-     do b ← p (a.fget idx);
+     do b ← p (a.get idx);
      match b with
      | true  => pure true
      | false => anyMAux (i+1)
@@ -275,7 +279,7 @@ variable {β : Type v}
 | 0,   h, b => pure b
 | j+1, h, b => do
   let i : Fin a.size := ⟨j, h⟩;
-  b ← f i (a.fget i) b;
+  b ← f i (a.get i) b;
   miterateRevAux j (Nat.leOfLt h) b
 
 @[inline] def miterateRev (a : Array α) (b : β) (f : ∀ (i : Fin a.size), α → β → m β) : m β :=
@@ -309,9 +313,9 @@ variable {β:Type u}
 | i, a =>
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩;
-     let v   : α          := a.fget idx;
-     let a                := a.fset idx (@unsafeCast _ _ ⟨v⟩ ());
-     do newV ← f i v; ummapAux (i+1) (a.fset idx (@unsafeCast _ _ ⟨v⟩ newV))
+     let v   : α          := a.get idx;
+     let a                := a.set idx (@unsafeCast _ _ ⟨v⟩ ());
+     do newV ← f i v; ummapAux (i+1) (a.set idx (@unsafeCast _ _ ⟨v⟩ newV))
   else
      pure (unsafeCast a)
 
@@ -334,10 +338,10 @@ variable {β:Type u}
 @[inline] def modify [Inhabited α] (a : Array α) (i : Nat) (f : α → α) : Array α :=
 if h : i < a.size then
   let idx : Fin a.size := ⟨i, h⟩;
-  let v                := a.fget idx;
-  let a                := a.fset idx (default α);
+  let v                := a.get idx;
+  let a                := a.set idx (arbitrary α);
   let v                := f v;
-  a.fset idx v
+  a.set idx v
 else
   a
 
@@ -357,7 +361,7 @@ partial def mforAux {α : Type w} {β : Type u} (f : α → m β) (a : Array α)
 | i =>
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩;
-     let v   : α          := a.fget idx;
+     let v   : α          := a.get idx;
      f v *> mforAux (i+1)
   else
      pure ⟨⟩
@@ -372,7 +376,7 @@ partial def extractAux (a : Array α) : Nat → ∀ (e : Nat), e ≤ a.size →
 | i, e, hle, r =>
   if hlt : i < e then
     let idx : Fin a.size := ⟨i, Nat.ltOfLtOfLe hlt hle⟩;
-    extractAux (i+1) e hle (r.push (a.fget idx))
+    extractAux (i+1) e hle (r.push (a.get idx))
  else r
 
 def extract (a : Array α) (b e : Nat) : Array α :=
@@ -391,7 +395,7 @@ partial def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α →
   if h : i < a.size then
      let aidx : Fin a.size := ⟨i, h⟩;
      let bidx : Fin b.size := ⟨i, hsz ▸ h⟩;
-     match p (a.fget aidx) (b.fget bidx) with
+     match p (a.get aidx) (b.get bidx) with
      | true  => isEqvAux (i+1)
      | false => false
   else
@@ -411,7 +415,7 @@ partial def reverseAux : Array α → Nat → Array α
 | a, i =>
   let n := a.size;
   if i < n / 2 then
-    reverseAux (a.swap i (n - i - 1)) (i+1)
+    reverseAux (a.swap! i (n - i - 1)) (i+1)
   else
     a
 
@@ -422,9 +426,9 @@ reverseAux a 0
 @[specialize] partial def filterAux (p : α → Bool) : Array α → Nat → Nat → Array α
 | a, i, j =>
   if h₁ : i < a.size then
-    if p (a.fget ⟨i, h₁⟩) then
+    if p (a.get ⟨i, h₁⟩) then
        if h₂ : j < i then
-         filterAux (a.fswap ⟨i, h₁⟩ ⟨j, Nat.ltTrans h₂ h₁⟩) (i+1) (j+1)
+         filterAux (a.swap ⟨i, h₁⟩ ⟨j, Nat.ltTrans h₂ h₁⟩) (i+1) (j+1)
        else
          filterAux a (i+1) (j+1)
     else
@@ -439,7 +443,7 @@ partial def indexOfAux {α} [HasBeq α] (a : Array α) (v : α) : Nat → Option
 | i =>
   if h : i < a.size then
     let idx : Fin a.size := ⟨i, h⟩;
-    if a.fget idx == v then some idx
+    if a.get idx == v then some idx
     else indexOfAux (i+1)
   else none
 
@@ -451,7 +455,7 @@ partial def eraseIdxAux {α} : Nat → Array α → Array α
   if h : i < a.size then
     let idx  : Fin a.size := ⟨i, h⟩;
     let idx1 : Fin a.size := ⟨i - 1, Nat.ltOfLeOfLt (Nat.predLe i) h⟩;
-    eraseIdxAux (i+1) (a.fswap idx idx1)
+    eraseIdxAux (i+1) (a.swap idx idx1)
   else
     a.pop
 
@@ -461,7 +465,7 @@ eraseIdxAux (i.val + 1) a
 def eraseIdx {α} (a : Array α) (i : Nat) : Array α :=
 if i < a.size then eraseIdxAux (i+1) a else a
 
-theorem szFSwapEq (a : Array α) (i j : Fin a.size) : (a.fswap i j).size = a.size :=
+theorem szFSwapEq (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size :=
 rfl
 
 theorem szPopEq (a : Array α) : a.pop.size = a.size - 1 :=
@@ -478,7 +482,7 @@ partial def eraseIdxSzAux {α} (a : Array α) : ∀ (i : Nat) (r : Array α), r.
   if h : i < r.size then
     let idx  : Fin r.size := ⟨i, h⟩;
     let idx1 : Fin r.size := ⟨i - 1, Nat.ltOfLeOfLt (Nat.predLe i) h⟩;
-    eraseIdxSzAux (i+1) (r.fswap idx idx1) ((szFSwapEq r idx idx1).trans heq)
+    eraseIdxSzAux (i+1) (r.swap idx idx1) ((szFSwapEq r idx idx1).trans heq)
   else
     ⟨r.pop, (szPopEq r).trans (heq ▸ rfl)⟩
 end
diff --git a/library/init/data/array/binsearch.lean b/library/init/data/array/binsearch.lean
index bde19f3697..3a904d6810 100644
--- a/library/init/data/array/binsearch.lean
+++ b/library/init/data/array/binsearch.lean
@@ -15,7 +15,7 @@ namespace Array
 | lo, hi =>
   if lo <= hi then
     let m := (lo + hi)/2;
-    let a := as.get m;
+    let a := as.get! m;
     if lt a k then binSearchAux (m+1) hi
     else if lt k a then
       if m == 0 then found none
diff --git a/library/init/data/array/qsort.lean b/library/init/data/array/qsort.lean
index 14152e3f26..934e124d0f 100644
--- a/library/init/data/array/qsort.lean
+++ b/library/init/data/array/qsort.lean
@@ -13,21 +13,21 @@ namespace Array
 @[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : α → α → Bool) (hi : Nat) (pivot : α) : Array α → Nat → Nat → Nat × Array α
 | as, i, j =>
   if j < hi then
-    if lt (as.get j) pivot then
-      let as := as.swap i j;
+    if lt (as.get! j) pivot then
+      let as := as.swap! i j;
       partitionAux as (i+1) (j+1)
     else
       partitionAux as i (j+1)
   else
-    let as := as.swap i hi;
+    let as := as.swap! i hi;
     (i, as)
 
 @[inline] def partition {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat × Array α :=
 let mid := (lo + hi) / 2;
-let as  := if lt (as.get mid) (as.get lo) then as.swap lo mid else as;
-let as  := if lt (as.get hi)  (as.get lo) then as.swap lo hi  else as;
-let as  := if lt (as.get mid) (as.get hi) then as.swap mid hi else as;
-let pivot := as.get hi;
+let as  := if lt (as.get! mid) (as.get! lo) then as.swap! lo mid else as;
+let as  := if lt (as.get! hi)  (as.get! lo) then as.swap! lo hi  else as;
+let as  := if lt (as.get! mid) (as.get! hi) then as.swap! mid hi else as;
+let pivot := as.get! hi;
 partitionAux lt hi pivot as lo lo
 
 @[specialize] partial def qsortAux {α : Type} [Inhabited α] (lt : α → α → Bool) : Array α → Nat → Nat → Array α
diff --git a/library/init/data/bytearray/basic.lean b/library/init/data/bytearray/basic.lean
index f16f89d816..f5a98cb6bb 100644
--- a/library/init/data/bytearray/basic.lean
+++ b/library/init/data/bytearray/basic.lean
@@ -33,12 +33,12 @@ def size : (@& ByteArray) → Nat
 | ⟨bs⟩ => bs.size
 
 @[extern "lean_byte_array_get"]
-def get : (@& ByteArray) → (@& Nat) → UInt8
-| ⟨bs⟩, i => bs.get i
+def get! : (@& ByteArray) → (@& Nat) → UInt8
+| ⟨bs⟩, i => bs.get! i
 
 @[extern "lean_byte_array_set"]
-def set : ByteArray → (@& Nat) → UInt8 → ByteArray
-| ⟨bs⟩, i, b => ⟨bs.set i b⟩
+def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
+| ⟨bs⟩, i, b => ⟨bs.set! i b⟩
 
 def isEmpty (s : ByteArray) : Bool :=
 s.size == 0
@@ -46,7 +46,7 @@ s.size == 0
 partial def toListAux (bs : ByteArray) : Nat → List UInt8 → List UInt8
 | i, r =>
   if i < bs.size then
-    toListAux (i+1) (bs.get i :: r)
+    toListAux (i+1) (bs.get! i :: r)
   else
     r.reverse
 
diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean
index a512dfc44d..f5a7868dff 100644
--- a/library/init/data/hashmap/basic.lean
+++ b/library/init/data/hashmap/basic.lean
@@ -71,9 +71,9 @@ partial def moveEntries [Hashable α] : Nat → Array (AssocList α β) → Hash
 | i, source, target =>
   if h : i < source.size then
      let idx : Fin source.size := ⟨i, h⟩;
-     let es  : AssocList α β   := source.fget idx;
+     let es  : AssocList α β   := source.get idx;
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
-     let source                := source.fset idx AssocList.nil;
+     let source                := source.set idx AssocList.nil;
      let target                := es.foldl (reinsertAux hash) target;
      moveEntries (i+1) source target
   else target
diff --git a/library/init/data/persistentarray/basic.lean b/library/init/data/persistentarray/basic.lean
index a89633b6ec..d14ae5ca62 100644
--- a/library/init/data/persistentarray/basic.lean
+++ b/library/init/data/persistentarray/basic.lean
@@ -58,12 +58,12 @@ abbrev div2Shift (i : USize) (shift : USize) : USize := USize.shift_right i shif
 abbrev mod2Shift (i : USize) (shift : USize) : USize := USize.land i ((USize.shift_left 1 shift) - 1)
 
 partial def getAux [Inhabited α] : PersistentArrayNode α → USize → USize → α
-| node cs, i, shift => getAux (cs.get (div2Shift i shift).toNat) (mod2Shift i shift) (shift - initShift)
-| leaf cs, i, _     => cs.get i.toNat
+| node cs, i, shift => getAux (cs.get! (div2Shift i shift).toNat) (mod2Shift i shift) (shift - initShift)
+| leaf cs, i, _     => cs.get! i.toNat
 
 def get [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 if i >= t.tailOff then
-  t.tail.get (i - t.tailOff)
+  t.tail.get! (i - t.tailOff)
 else
   getAux t.root (USize.ofNat i) t.shift
 
@@ -73,11 +73,11 @@ partial def setAux : PersistentArrayNode α → USize → USize → α → Persi
   let i     := mod2Shift i shift;
   let shift := shift - initShift;
   node $ cs.modify j.toNat $ fun c => setAux c i shift a
-| leaf cs, i, _,     a => leaf (cs.set i.toNat a)
+| leaf cs, i, _,     a => leaf (cs.set! i.toNat a)
 
 def set (t : PersistentArray α) (i : Nat) (a : α) : PersistentArray α :=
 if i >= t.tailOff then
-  { tail := t.tail.set (i - t.tailOff) a, .. t }
+  { tail := t.tail.set! (i - t.tailOff) a, .. t }
 else
   { root := setAux t.root (USize.ofNat i) t.shift a, .. t }
 
@@ -145,8 +145,8 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
 | n@(node cs) =>
   if h : cs.size ≠ 0 then
     let idx : Fin cs.size := ⟨cs.size - 1, Nat.predLt h⟩;
-    let last := cs.fget idx;
-    let cs   := cs.fset idx (default _);
+    let last := cs.get idx;
+    let cs   := cs.set idx (default _);
     match popLeaf last with
     | (none,   _)       => (none, emptyArray)
     | (some l, newLast) =>
@@ -154,7 +154,7 @@ partial def popLeaf : PersistentArrayNode α → Option (Array α) × Array (Per
         let cs := cs.pop;
         if cs.isEmpty then (some l, emptyArray) else (some l, cs)
       else
-        (some l, cs.fset idx (node newLast))
+        (some l, cs.set idx (node newLast))
   else
     (none, emptyArray)
 | leaf vs   => (some vs, emptyArray)
@@ -169,8 +169,8 @@ else
     let last       := last.pop;
     let newSize    := t.size - 1;
     let newTailOff := newSize - last.size;
-    if newRoots.size == 1 && (newRoots.get 0).isNode then
-      { root    := newRoots.get 0,
+    if newRoots.size == 1 && (newRoots.get! 0).isNode then
+      { root    := newRoots.get! 0,
         shift   := t.shift - initShift,
         size    := newSize,
         tail    := last,
@@ -216,7 +216,7 @@ do b ← t.tail.mfindRev f;
 partial def mfoldlFromAux (f : β → α → m β) : PersistentArrayNode α → USize → USize → β → m β
 | node cs, i, shift, b => do
   let j    := (div2Shift i shift).toNat;
-  b ← mfoldlFromAux (cs.get j) (mod2Shift i shift) (shift - initShift) b;
+  b ← mfoldlFromAux (cs.get! j) (mod2Shift i shift) (shift - initShift) b;
   cs.mfoldlFrom (fun b c => mfoldlAux f c b) b (j+1)
 | leaf vs, i, _, b => vs.mfoldlFrom f b i.toNat
 
diff --git a/library/init/data/persistenthashmap/basic.lean b/library/init/data/persistenthashmap/basic.lean
index dee036b317..46849b1940 100644
--- a/library/init/data/persistenthashmap/basic.lean
+++ b/library/init/data/persistenthashmap/basic.lean
@@ -68,10 +68,10 @@ inductive IsEntriesNode : Node α β → Prop
 
 abbrev EntriesNode (α β) := { n : Node α β // IsEntriesNode n }
 
-private theorem fsetSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (i : Fin ks.size) (j : Fin vs.size) (k : α) (v : β)
-                           : (ks.fset i k).size = (vs.fset j v).size :=
-have h₁ : (ks.fset i k).size = ks.size from Array.szFSetEq _ _ _;
-have h₂ : (vs.fset j v).size = vs.size from Array.szFSetEq _ _ _;
+private theorem setSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (i : Fin ks.size) (j : Fin vs.size) (k : α) (v : β)
+                           : (ks.set i k).size = (vs.set j v).size :=
+have h₁ : (ks.set i k).size = ks.size from Array.szFSetEq _ _ _;
+have h₂ : (vs.set j v).size = vs.size from Array.szFSetEq _ _ _;
 (h₁.trans h).trans h₂.symm
 
 private theorem pushSizeEq {ks : Array α} {vs : Array β} (h : ks.size = vs.size) (k : α) (v : β) : (ks.push k).size = (vs.push v).size :=
@@ -84,10 +84,10 @@ partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat 
 | n@⟨Node.collision keys vals heq, _⟩, i, k, v =>
   if h : i < keys.size then
     let idx : Fin keys.size := ⟨i, h⟩;
-    let k' := keys.fget idx;
+    let k' := keys.get idx;
     if k == k' then
        let j : Fin vals.size := ⟨i, heq ▸ h⟩;
-       ⟨Node.collision (keys.fset idx k) (vals.fset j v) (fsetSizeEq heq idx j k v), IsCollisionNode.mk _ _ _⟩
+       ⟨Node.collision (keys.set idx k) (vals.set j v) (setSizeEq heq idx j k v), IsCollisionNode.mk _ _ _⟩
     else insertAtCollisionNodeAux n (i+1) k v
   else
     ⟨Node.collision (keys.push k) (vals.push v) (pushSizeEq heq k v), IsCollisionNode.mk _ _ _⟩
@@ -116,7 +116,7 @@ partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize
     | ⟨Node.collision keys vals heq, _⟩ =>
       let entries : Node α β := mkEmptyEntries;
       keys.iterate entries $ fun i k entries =>
-        let v := vals.fget ⟨i.val, heq ▸ i.isLt⟩;
+        let v := vals.get ⟨i.val, heq ▸ i.isLt⟩;
         let h := hash k;
         -- dbgTrace ("toCollision " ++ toString i ++ ", h: " ++ toString h ++ ", depth: " ++ toString depth ++ ", h': " ++
         --          toString (div2Shift h (shift * (depth - 1)))) $ fun _ =>
@@ -138,15 +138,15 @@ def insert [HasBeq α] [Hashable α] : PersistentHashMap α β → α → β →
 partial def findAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option β
 | i, k =>
   if h : i < keys.size then
-    let k' := keys.fget ⟨i, h⟩;
-    if k == k' then some (vals.fget ⟨i, heq ▸ h⟩)
+    let k' := keys.get ⟨i, h⟩;
+    if k == k' then some (vals.get ⟨i, heq ▸ h⟩)
     else findAtAux (i+1) k
   else none
 
 partial def findAux [HasBeq α] : Node α β → USize → α → Option β
 | Node.entries entries, h, k =>
   let j     := (mod2Shift h shift).toNat;
-  match entries.get j with
+  match entries.get! j with
   | Entry.null       => none
   | Entry.ref node   => findAux node (div2Shift h shift) k
   | Entry.entry k' v => if k == k' then some v else none
@@ -161,7 +161,7 @@ def find [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Option 
 partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Bool
 | i, k =>
   if h : i < keys.size then
-    let k' := keys.fget ⟨i, h⟩;
+    let k' := keys.get ⟨i, h⟩;
     if k == k' then true
     else containsAtAux (i+1) k
   else false
@@ -169,7 +169,7 @@ partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq :
 partial def containsAux [HasBeq α] : Node α β → USize → α → Bool
 | Node.entries entries, h, k =>
   let j     := (mod2Shift h shift).toNat;
-  match entries.get j with
+  match entries.get! j with
   | Entry.null       => false
   | Entry.ref node   => containsAux node (div2Shift h shift) k
   | Entry.entry k' v => k == k'
@@ -181,7 +181,7 @@ def contains [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Bool
 partial def isUnaryEntries (a : Array (Entry α β (Node α β))) : Nat → Option (α × β) → Option (α × β)
 | i, acc =>
   if h : i < a.size then
-    match a.fget ⟨i, h⟩ with
+    match a.get ⟨i, h⟩ with
     | Entry.null      => isUnaryEntries (i+1) acc
     | Entry.ref _     => none
     | Entry.entry k v =>
@@ -195,7 +195,7 @@ def isUnaryNode : Node α β → Option (α × β)
 | Node.collision keys vals heq =>
   if h : 1 = keys.size then
     have 0 < keys.size from h ▸ (Nat.zeroLtSucc _);
-    some (keys.fget ⟨0, this⟩, vals.fget ⟨0, heq ▸ this⟩)
+    some (keys.get ⟨0, this⟩, vals.get ⟨0, heq ▸ this⟩)
   else
     none
 
@@ -210,18 +210,18 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β ×
   | none     => (n, false)
 | n@(Node.entries entries), h, k =>
   let j       := (mod2Shift h shift).toNat;
-  let entry   := entries.get j;
+  let entry   := entries.get! j;
   match entry with
   | Entry.null       => (n, false)
   | Entry.entry k' v =>
-    if k == k' then (Node.entries (entries.set j Entry.null), true) else (n, false)
+    if k == k' then (Node.entries (entries.set! j Entry.null), true) else (n, false)
   | Entry.ref node   =>
-    let entries := entries.set j Entry.null;
+    let entries := entries.set! j Entry.null;
     let (newNode, deleted) := eraseAux node (div2Shift h shift) k;
     if !deleted then (n, false)
     else match isUnaryNode newNode with
-      | none        => (Node.entries (entries.set j (Entry.ref newNode)), true)
-      | some (k, v) => (Node.entries (entries.set j (Entry.entry k v)), true)
+      | none        => (Node.entries (entries.set! j (Entry.ref newNode)), true)
+      | some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true)
 
 def erase [HasBeq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
 | { root := n, size := sz }, k =>
@@ -234,7 +234,7 @@ variables {m : Type w → Type w'} [Monad m]
 variables {σ : Type w}
 
 @[specialize] partial def mfoldlAux (f : σ → α → β → m σ) : Node α β → σ → m σ
-| Node.collision keys vals heq, acc => keys.miterate acc $ fun i k acc => f acc k (vals.fget ⟨i.val, heq ▸ i.isLt⟩)
+| Node.collision keys vals heq, acc => keys.miterate acc $ fun i k acc => f acc k (vals.get ⟨i.val, heq ▸ i.isLt⟩)
 | Node.entries entries, acc => entries.mfoldl (fun acc entry =>
   match entry with
   | Entry.null      => pure acc
diff --git a/library/init/lean/attributes.lean b/library/init/lean/attributes.lean
index 29bd4d5b7d..79b8e4bffd 100644
--- a/library/init/lean/attributes.lean
+++ b/library/init/lean/attributes.lean
@@ -309,7 +309,7 @@ end EnumAttributes
 def attrParamSyntaxToIdentifier (s : Syntax) : Option Name :=
 match s with
 | Syntax.node k args =>
-  if k == nullKind && args.size == 1 then match args.get 0 with
+  if k == nullKind && args.size == 1 then match args.get! 0 with
     | Syntax.ident _ _ id _ => some id
     | _ => none
   else
diff --git a/library/init/lean/compiler/externattr.lean b/library/init/lean/compiler/externattr.lean
index 42d95b25a2..70664b6100 100644
--- a/library/init/lean/compiler/externattr.lean
+++ b/library/init/lean/compiler/externattr.lean
@@ -41,18 +41,18 @@ instance ExternAttrData.inhabited : Inhabited ExternAttrData := ⟨{ entries :=
 private partial def syntaxToExternEntries (a : Array Syntax) : Nat → List ExternEntry → Except String (List ExternEntry)
 | i, entries =>
   if i == a.size then Except.ok entries
-  else match a.get i with
+  else match a.get! i with
     | Syntax.ident _ _ backend _ =>
       let i := i + 1;
       if i == a.size then Except.error "string or identifier expected"
-      else match (a.get i).isIdOrAtom with
+      else match (a.get! i).isIdOrAtom with
         | some "adhoc"  => syntaxToExternEntries (i+1) (ExternEntry.adhoc backend :: entries)
         | some "inline" =>
           let i := i + 1;
-          match (a.get i).isStrLit with
+          match (a.get! i).isStrLit with
           | some pattern => syntaxToExternEntries (i+1) (ExternEntry.inline backend pattern :: entries)
           | none => Except.error "string literal expected"
-        | _ => match (a.get i).isStrLit with
+        | _ => match (a.get! i).isStrLit with
           | some fn => syntaxToExternEntries (i+1) (ExternEntry.standard backend fn :: entries)
           | none => Except.error "string literal expected"
     | _ => Except.error "identifier expected"
@@ -63,10 +63,10 @@ match s with
 | Syntax.node _ args =>
   if args.size == 0 then Except.error "unexpected kind of argument"
   else
-    let (arity, i) : Option Nat × Nat := match (args.get 0).isNatLit with
+    let (arity, i) : Option Nat × Nat := match (args.get! 0).isNatLit with
       | some arity => (some arity, 1)
       | none       => (none, 0);
-    match (args.get i).isStrLit with
+    match (args.get! i).isStrLit with
     | some str =>
       if args.size == i+1 then
         Except.ok { arity := arity, entries := [ ExternEntry.standard `all str ] }
diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean
index e90450ecde..eae337d369 100644
--- a/library/init/lean/compiler/ir/basic.lean
+++ b/library/init/lean/compiler/ir/basic.lean
@@ -342,7 +342,7 @@ partial def reshapeAux : Array FnBody → Nat → FnBody → FnBody
   if i == 0 then b
   else
     let i         := i - 1;
-    let (curr, a) := a.swapAt i (default _);
+    let (curr, a) := a.swapAt! i (default _);
     let b         := curr.setBody b;
     reshapeAux a i b
 
diff --git a/library/init/lean/compiler/ir/borrow.lean b/library/init/lean/compiler/ir/borrow.lean
index 8a6f2762ac..c280972141 100644
--- a/library/init/lean/compiler/ir/borrow.lean
+++ b/library/init/lean/compiler/ir/borrow.lean
@@ -190,8 +190,8 @@ match s.map.find k with
 /- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/
 def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=
 xs.size.mfor $ fun i => do
-  let x := xs.get i;
-  let p := ps.get i;
+  let x := xs.get! i;
+  let p := ps.get! i;
   unless p.borrow $ ownArg x
 
 /- For each xs[i], if xs[i] is owned, then mark ps[i] as owned.
@@ -201,8 +201,8 @@ xs.size.mfor $ fun i => do
    "break" the tail call. -/
 def ownParamsUsingArgs (xs : Array Arg) (ps : Array Param) : M Unit :=
 xs.size.mfor $ fun i => do
-  let x := xs.get i;
-  let p := ps.get i;
+  let x := xs.get! i;
+  let p := ps.get! i;
   match x with
   | Arg.var x => mwhen (isOwned x) $ ownVar p.x
   | _         => pure ()
diff --git a/library/init/lean/compiler/ir/boxing.lean b/library/init/lean/compiler/ir/boxing.lean
index 2363004a16..f9a03ea028 100644
--- a/library/init/lean/compiler/ir/boxing.lean
+++ b/library/init/lean/compiler/ir/boxing.lean
@@ -57,8 +57,8 @@ qs ← ps.mmap (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.o
 (newVDecls, xs) ← qs.size.mfold
   (fun i (r : Array FnBody × Array Arg) =>
      let (newVDecls, xs) := r;
-     let p := ps.get i;
-     let q := qs.get i;
+     let p := ps.get! i;
+     let q := qs.get! i;
      if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x))
      else do
        x ← mkFresh;
@@ -242,7 +242,7 @@ xs.miterate (Array.empty, Array.empty) $ fun i (x : Arg) (r : Array Arg × Array
       pure (xs.push (Arg.var y), bs.push b)
 
 @[inline] def castArgsIfNeeded (xs : Array Arg) (ps : Array Param) (k : Array Arg → M FnBody) : M FnBody :=
-do (ys, bs) ← castArgsIfNeededAux xs (fun i => (ps.get i).ty);
+do (ys, bs) ← castArgsIfNeededAux xs (fun i => (ps.get! i).ty);
    b ← k ys;
    pure (reshape bs b)
 
diff --git a/library/init/lean/compiler/ir/emitc.lean b/library/init/lean/compiler/ir/emitc.lean
index 854ea6f113..578a2eeeee 100644
--- a/library/init/lean/compiler/ir/emitc.lean
+++ b/library/init/lean/compiler/ir/emitc.lean
@@ -104,7 +104,7 @@ unless (ps.isEmpty) $ do {
   else
     ps.size.mfor $ fun i => do {
       when (i > 0) (emit ", ");
-      emit (toCType (ps.get i).ty)
+      emit (toCType (ps.get! i).ty)
     };
   emit ")"
 };
@@ -257,8 +257,8 @@ else
 
 def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) :=
 if alts.size != 2 then none
-else match alts.get 0 with
-  | Alt.ctor c b => some (c.cidx, b, (alts.get 1).body)
+else match alts.get! 0 with
+  | Alt.ctor c b => some (c.cidx, b, (alts.get! 1).body)
   | _            => none
 
 def emitIf (emitBody : FnBody → M Unit) (x : VarId) (xType : IRType) (tag : Nat) (t : FnBody) (e : FnBody) : M Unit :=
@@ -330,8 +330,8 @@ do
   ps ← getJPParams j;
   unless (xs.size == ps.size) (throw "invalid goto");
   xs.size.mfor $ fun i => do {
-    let p := ps.get i;
-    let x := xs.get i;
+    let p := ps.get! i;
+    let x := xs.get! i;
     emit p.x; emit " = "; emitArg x; emitLn ";"
   };
   emit "goto "; emit j; emitLn ";"
@@ -342,7 +342,7 @@ do emit z; emit " = "
 def emitArgs (ys : Array Arg) : M Unit :=
 ys.size.mfor $ fun i => do
   when (i > 0) (emit ", ");
-  emitArg (ys.get i)
+  emitArg (ys.get! i)
 
 def emitCtorScalarSize (usize : Nat) (ssize : Nat) : M Unit :=
 if usize == 0 then emit ssize
@@ -356,7 +356,7 @@ emitCtorScalarSize c.usize c.ssize; emitLn ");"
 
 def emitCtorSetArgs (z : VarId) (ys : Array Arg) : M Unit :=
 ys.size.mfor $ fun i => do
-  emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg (ys.get i); emitLn ");"
+  emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg (ys.get! i); emitLn ");"
 
 def emitCtor (z : VarId) (c : CtorInfo) (ys : Array Arg) : M Unit :=
 do
@@ -426,7 +426,7 @@ decl ← getDecl f;
 let arity := decl.params.size;
 emitLhs z; emit "lean_alloc_closure((void*)("; emitCName f; emit "), "; emit arity; emit ", "; emit ys.size; emitLn ");";
 ys.size.mfor $ fun i => do {
-   let y := ys.get i;
+   let y := ys.get! i;
    emit "lean_closure_set("; emit z; emit ", "; emit i; emit ", "; emitArg y; emitLn ");"
 }
 
@@ -545,8 +545,8 @@ That is, we have
 def overwriteParam (ps : Array Param) (ys : Array Arg) : Bool :=
 let n := ps.size;
 n.any $ fun i =>
-  let p := ps.get i;
-  (i+1, n).anyI $ fun j => paramEqArg p (ys.get j)
+  let p := ps.get! i;
+  (i+1, n).anyI $ fun j => paramEqArg p (ys.get! j)
 
 def emitTailCall (v : Expr) : M Unit :=
 match v with
@@ -557,22 +557,22 @@ match v with
   if overwriteParam ps ys then do {
     emitLn "{";
     ps.size.mfor $ fun i => do {
-      let p := ps.get i;
-      let y := ys.get i;
+      let p := ps.get! i;
+      let y := ys.get! i;
       unless (paramEqArg p y) $ do {
         emit (toCType p.ty); emit " _tmp_"; emit i; emit " = "; emitArg y; emitLn ";"
       }
     };
     ps.size.mfor $ fun i => do {
-      let p := ps.get i;
-      let y := ys.get i;
+      let p := ps.get! i;
+      let y := ys.get! i;
       unless (paramEqArg p y) (do emit p.x; emit " = _tmp_"; emit i; emitLn ";")
     };
     emitLn "}"
   } else do {
     ys.size.mfor $ fun i => do {
-      let p := ps.get i;
-      let y := ys.get i;
+      let p := ps.get! i;
+      let y := ys.get! i;
       unless (paramEqArg p y) (do emit p.x; emit " = "; emitArg y; emitLn ";")
     }
   };
@@ -627,7 +627,7 @@ unless (hasInitAttr env d.name) $
       else
         xs.size.mfor $ fun i => do {
           when (i > 0) (emit ", ");
-          let x := xs.get i;
+          let x := xs.get! i;
           emit (toCType x.ty); emit " "; emit x.x
         };
       emit ")"
@@ -637,7 +637,7 @@ unless (hasInitAttr env d.name) $
     emitLn " {";
     when (xs.size > closureMaxArgs && isBoxedName d.name) $
       xs.size.mfor $ fun i => do {
-        let x := xs.get i;
+        let x := xs.get! i;
         emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];"
       };
     emitLn "_start:";
diff --git a/library/init/lean/compiler/ir/expandresetreuse.lean b/library/init/lean/compiler/ir/expandresetreuse.lean
index 492d45d2e8..b8b8660437 100644
--- a/library/init/lean/compiler/ir/expandresetreuse.lean
+++ b/library/init/lean/compiler/ir/expandresetreuse.lean
@@ -67,7 +67,7 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB
     | (FnBody.vdecl _ _ (Expr.uproj _ _) _)   => keepInstr b
     | (FnBody.inc z n c p _) =>
       if n == 0 then done () else
-      let b' := bs.get (bs.size - 2);
+      let b' := bs.get! (bs.size - 2);
       match b' with
       | (FnBody.vdecl w _ (Expr.proj i x) _) =>
         if w == z && y == x then
@@ -79,7 +79,7 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB
              We keep `proj`, and `inc` when `n > 1`
           -/
           let bs   := bs.pop.pop;
-          let mask := mask.set i (some z);
+          let mask := mask.set! i (some z);
           let keep := keep.push b';
           let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c p FnBody.nil);
           eraseProjIncForAux bs mask keep
@@ -142,7 +142,7 @@ modifyGet $ fun n => ({ idx := n }, n + 1)
 def releaseUnreadFields (y : VarId) (mask : Mask) (b : FnBody) : M FnBody :=
 mask.size.mfold
   (fun i b =>
-    match mask.get i with
+    match mask.get! i with
     | some _ => pure b -- code took ownership of this field
     | none   => do
       fld ← mkFresh;
@@ -151,7 +151,7 @@ mask.size.mfold
 
 def setFields (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody :=
 zs.size.fold
-  (fun i b => FnBody.set y i (zs.get i) b)
+  (fun i b => FnBody.set y i (zs.get! i) b)
   b
 
 /- Given `set x[i] := y`, return true iff `y := proj[i] x` -/
diff --git a/library/init/lean/compiler/ir/pushproj.lean b/library/init/lean/compiler/ir/pushproj.lean
index ad4032f4bb..b18fcf3da4 100644
--- a/library/init/lean/compiler/ir/pushproj.lean
+++ b/library/init/lean/compiler/ir/pushproj.lean
@@ -21,7 +21,7 @@ partial def pushProjs : Array FnBody → Array Alt → Array IndexSet → Array
     let push (x : VarId) (t : IRType) (v : Expr) :=
         if !ctxF.contains x.idx then
           let alts := alts.mapIdx $ fun i alt => alt.modifyBody $ fun b' =>
-             if (altsF.get i).contains x.idx then b.setBody b'
+             if (altsF.get! i).contains x.idx then b.setBody b'
              else b';
           let altsF  := altsF.map $ fun s => if s.contains x.idx then b.collectFreeIndices s else s;
           pushProjs bs alts altsF ctx ctxF
diff --git a/library/init/lean/compiler/ir/rc.lean b/library/init/lean/compiler/ir/rc.lean
index 5c2e722571..828f2d2f77 100644
--- a/library/init/lean/compiler/ir/rc.lean
+++ b/library/init/lean/compiler/ir/rc.lean
@@ -77,21 +77,21 @@ caseLiveVars.fold
 
 /- `isFirstOcc xs x i = true` if `xs[i]` is the first occurrence of `xs[i]` in `xs` -/
 private def isFirstOcc (xs : Array Arg) (i : Nat) : Bool :=
-let x := xs.get i;
-i.all $ fun j => xs.get j != x
+let x := xs.get! i;
+i.all $ fun j => xs.get! j != x
 
 /- Return true if `x` also occurs in `ys` in a position that is not consumed.
    That is, it is also passed as a borrow reference. -/
 @[specialize]
 private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Bool :=
 ys.size.any $ fun i =>
-  let y := ys.get i;
+  let y := ys.get! i;
   match y with
   | Arg.irrelevant => false
   | Arg.var y      => x == y && !consumeParamPred i
 
 private def isBorrowParam (x : VarId) (ys : Array Arg) (ps : Array Param) : Bool :=
-isBorrowParamAux x ys (fun i => !(ps.get i).borrow)
+isBorrowParamAux x ys (fun i => not (ps.get! i).borrow)
 
 /-
 Return `n`, the number of times `x` is consumed.
@@ -102,7 +102,7 @@ Return `n`, the number of times `x` is consumed.
 private def getNumConsumptions (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Nat :=
 ys.size.fold
   (fun i n =>
-    let y := ys.get i;
+    let y := ys.get! i;
     match y with
     | Arg.irrelevant => n
     | Arg.var y      => if x == y && consumeParamPred i then n+1 else n)
@@ -112,7 +112,7 @@ ys.size.fold
 private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : Nat → Bool) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
 xs.size.fold
   (fun i b =>
-    let x := xs.get i;
+    let x := xs.get! i;
     match x with
     | Arg.irrelevant => b
     | Arg.var x =>
@@ -133,13 +133,13 @@ xs.size.fold
   b
 
 private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
-addIncBeforeAux ctx xs (fun i => !(ps.get i).borrow) b liveVarsAfter
+addIncBeforeAux ctx xs (fun i => not (ps.get! i).borrow) b liveVarsAfter
 
 /- See `addIncBeforeAux`/`addIncBefore` for the procedure that inserts `inc` operations before an application.  -/
 private def addDecAfterFullApp (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=
 xs.size.fold
   (fun i b =>
-    match xs.get i with
+    match xs.get! i with
     | Arg.irrelevant => b
     | Arg.var x      =>
       /- We must add a `dec` if `x` must be consumed, it is alive after the application,
diff --git a/library/init/lean/compiler/ir/simpcase.lean b/library/init/lean/compiler/ir/simpcase.lean
index 0333951944..ba63605b04 100644
--- a/library/init/lean/compiler/ir/simpcase.lean
+++ b/library/init/lean/compiler/ir/simpcase.lean
@@ -19,14 +19,14 @@ else
   alts.push (Alt.default last.body)
 
 private def getOccsOf (alts : Array Alt) (i : Nat) : Nat :=
-let aBody := (alts.get i).body;
+let aBody := (alts.get! i).body;
 alts.iterateFrom 1 (i + 1) $ fun _ a' n =>
   if a'.body == aBody then n+1 else n
 
 private def maxOccs (alts : Array Alt) : Alt × Nat :=
-alts.iterateFrom (alts.get 0, getOccsOf alts 0) 1 $ fun i a p =>
+alts.iterateFrom (alts.get! 0, getOccsOf alts 0) 1 $ fun i a p =>
   let noccs := getOccsOf alts i.val;
-  if noccs > p.2 then (alts.fget i, noccs) else p
+  if noccs > p.2 then (alts.get i, noccs) else p
 
 private def addDefault (alts : Array Alt) : Array Alt :=
 if alts.size <= 1 || alts.any Alt.isDefault then alts
@@ -43,7 +43,7 @@ let alts := addDefault alts;
 if alts.size == 0 then
   FnBody.unreachable
 else if alts.size == 1 then
-  (alts.get 0).body
+  (alts.get! 0).body
 else
   FnBody.case tid x xType alts
 
diff --git a/library/init/lean/elaborator/preterm.lean b/library/init/lean/elaborator/preterm.lean
index 6d5e08cb77..f6f052d688 100644
--- a/library/init/lean/elaborator/preterm.lean
+++ b/library/init/lean/elaborator/preterm.lean
@@ -75,11 +75,11 @@ partial def toLevel : Syntax Expr → Elab Level
   | `Lean.Parser.Level.paren  => toLevel $ stx.getArg 1
   | `Lean.Parser.Level.max    => do
      let args := (stx.getArg 1).getArgs;
-     first ← toLevel (args.get 0);
+     first ← toLevel (args.get! 0);
      args.mfoldlFrom (fun r arg => Level.max r <$> toLevel arg) first 1
   | `Lean.Parser.Level.imax   => do
      let args := (stx.getArg 1).getArgs;
-     first ← toLevel (args.get 0);
+     first ← toLevel (args.get! 0);
      args.mfoldlFrom (fun r arg => Level.imax r <$> toLevel arg) first 1
   | `Lean.Parser.Level.hole   => pure $ Level.mvar Name.anonymous
   | `Lean.Parser.Level.num    => pure $ Level.ofNat $ (stx.getArg 0).toNat
diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean
index 45841e148a..d6b08eed77 100644
--- a/library/init/lean/environment.lean
+++ b/library/init/lean/environment.lean
@@ -128,13 +128,13 @@ structure EnvExtension (σ : Type) :=
 
 namespace EnvExtension
 unsafe def setStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment :=
-{ extensions := env.extensions.set ext.idx (unsafeCast s), .. env }
+{ extensions := env.extensions.set! ext.idx (unsafeCast s), .. env }
 
 @[implementedBy setStateUnsafe]
 constant setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment := default _
 
 unsafe def getStateUnsafe {σ : Type} (ext : EnvExtension σ) (env : Environment) : σ :=
-let s : EnvExtensionState := env.extensions.get ext.idx;
+let s : EnvExtensionState := env.extensions.get! ext.idx;
 @unsafeCast _ _ ⟨ext.stateInh⟩ s
 
 @[implementedBy getStateUnsafe]
@@ -232,7 +232,7 @@ instance PersistentEnvExtension.inhabited {α σ} [Inhabited σ] : Inhabited (Pe
 namespace PersistentEnvExtension
 
 def getModuleEntries {α σ : Type} (ext : PersistentEnvExtension α σ) (env : Environment) (m : ModuleIdx) : Array α :=
-(ext.toEnvExtension.getState env).importedEntries.get m
+(ext.toEnvExtension.getState env).importedEntries.get! m
 
 def addEntry {α σ : Type} (ext : PersistentEnvExtension α σ) (env : Environment) (a : α) : Environment :=
 ext.toEnvExtension.modifyState env $ fun s =>
@@ -347,11 +347,11 @@ unsafe def registerCPPExtension (initial : CPPExtensionState) : Option Nat :=
 
 @[export lean_set_extension]
 unsafe def setCPPExtensionState (env : Environment) (idx : Nat) (s : CPPExtensionState) : Option Environment :=
-(unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get idx).setState env s)).toOption
+(unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get! idx).setState env s)).toOption
 
 @[export lean_get_extension]
 unsafe def getCPPExtensionState (env : Environment) (idx : Nat) : Option CPPExtensionState :=
-(unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get idx).getState env)).toOption
+(unsafeIO (do exts ← envExtensionsRef.get; pure $ (exts.get! idx).getState env)).toOption
 end
 
 /- Legacy support for Modification objects -/
@@ -407,9 +407,9 @@ do
 pExts ← persistentEnvExtensionsRef.get;
 let entries : Array (Name × Array EnvExtensionEntry) := pExts.size.fold
   (fun i result =>
-    let state  := (pExts.get i).getState env;
-    let exportEntriesFn := (pExts.get i).exportEntriesFn;
-    let extName    := (pExts.get i).name;
+    let state  := (pExts.get! i).getState env;
+    let exportEntriesFn := (pExts.get! i).exportEntriesFn;
+    let extName    := (pExts.get! i).name;
     result.push (extName, exportEntriesFn state))
   Array.empty;
 bytes ← serializeModifications (modListExtension.getState env);
@@ -440,7 +440,7 @@ partial def importModulesAux : List Name → (NameSet × Array ModuleData) → I
 private partial def getEntriesFor (mod : ModuleData) (extId : Name) : Nat → Array EnvExtensionState
 | i =>
   if i < mod.entries.size then
-    let curr := mod.entries.get i;
+    let curr := mod.entries.get! i;
     if curr.1 == extId then curr.2 else getEntriesFor (i+1)
   else
     Array.empty
@@ -531,7 +531,7 @@ env.addAux cinfo
 def displayStats (env : Environment) : IO Unit :=
 do
 pExtDescrs ← persistentEnvExtensionsRef.get;
-let numModules := ((pExtDescrs.get 0).toEnvExtension.getState env).importedEntries.size;
+let numModules := ((pExtDescrs.get! 0).toEnvExtension.getState env).importedEntries.size;
 IO.println ("direct imports:                        " ++ toString env.header.imports);
 IO.println ("number of imported modules:            " ++ toString numModules);
 IO.println ("number of consts:                      " ++ toString env.constants.size);
diff --git a/library/init/lean/localcontext.lean b/library/init/lean/localcontext.lean
index 097a5e93f8..b9eeb0980e 100644
--- a/library/init/lean/localcontext.lean
+++ b/library/init/lean/localcontext.lean
@@ -237,7 +237,7 @@ isSubPrefixOfAux lctx₁.decls lctx₂.decls 0 0
 @[inline] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
 let b := b.abstract xs;
 xs.size.foldRev (fun i b =>
-  let x := xs.get i;
+  let x := xs.get! i;
   match lctx.findFVar x with
   | some (LocalDecl.cdecl _ _ n ty bi)  =>
     let ty := ty.abstractRange i xs;
diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 80f1aedfa6..98508390ff 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -1564,7 +1564,7 @@ variables {α β : Type} {m : Type → Type} [Monad m]
 @[specialize] partial def mfoldArgsAux (delta : Nat) (s : Array (Syntax α)) (f : Syntax α → β → m β) : Nat → β → m β
 | i, b =>
   if h : i < s.size then do
-    let curr := s.fget ⟨i, h⟩;
+    let curr := s.get ⟨i, h⟩;
     b ← f curr b;
     mfoldArgsAux (i+delta) b
   else
diff --git a/library/init/lean/parser/transform.lean b/library/init/lean/parser/transform.lean
index f0328fcdfa..175c2f91d1 100644
--- a/library/init/lean/parser/transform.lean
+++ b/library/init/lean/parser/transform.lean
@@ -16,13 +16,13 @@ match stx with
     match prevArg.getTailInfo with
     | some info =>
       let prevArg := prevArg.setTailInfo info.truncateTrailing;
-      let newArgs := newArgs.set (newArgs.size - 1) prevArg;
+      let newArgs := newArgs.set! (newArgs.size - 1) prevArg;
       let newArgs := newArgs.push (atom info sepTk);
       newArgs.push arg
     | none =>
       let newArgs := newArgs.push (atom none sepTk);
       newArgs.push arg)
-    (Array.singleton (args.get 0))
+    (Array.singleton (args.get! 0))
     1;
   node k args
 | stx => stx
diff --git a/library/init/lean/position.lean b/library/init/lean/position.lean
index d5814ec9c3..c20f5f41c2 100644
--- a/library/init/lean/position.lean
+++ b/library/init/lean/position.lean
@@ -62,12 +62,12 @@ private partial def toColumnAux (str : String) (lineBeginPos : String.Pos) (pos
 /- Remark: `pos` is in `[ps.get b, ps.get e]` and `b < e` -/
 private partial def toPositionAux (str : String) (ps : Array Nat) (lines : Array Nat) (pos : String.Pos) : Nat → Nat → Position
 | b, e =>
-  let posB := ps.get b;
-  if e == b + 1 then { line := lines.get b, column := toColumnAux str posB pos posB 0 }
+  let posB := ps.get! b;
+  if e == b + 1 then { line := lines.get! b, column := toColumnAux str posB pos posB 0 }
   else
     let m := (b + e) / 2;
-    let posM := ps.get m;
-    if pos == posM then { line := lines.get m, column := 0 }
+    let posM := ps.get! m;
+    if pos == posM then { line := lines.get! m, column := 0 }
     else if pos > posM then toPositionAux m e
     else toPositionAux b m
 
diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index bec55aa31e..a7b08bf4d8 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -91,7 +91,7 @@ match n with
 withArgs n $ fun args => args.size
 
 @[inline] def getArg {α} (n : SyntaxNode α) (i : Nat) : Syntax α :=
-withArgs n $ fun args => args.get i
+withArgs n $ fun args => args.get! i
 
 @[inline] def getArgs {α} (n : SyntaxNode α) : Array (Syntax α) :=
 withArgs n $ fun args => args
@@ -167,7 +167,7 @@ match stx with
 
 def setArg {α} (stx : Syntax α) (i : Nat) (arg : Syntax α) : Syntax α :=
 match stx with
-| node k args => node k (args.set i arg)
+| node k args => node k (args.set! i arg)
 | stx         => stx
 
 @[inline] def modifyArg {α} (stx : Syntax α) (i : Nat) (fn : Syntax α → Syntax α) : Syntax α :=
@@ -239,8 +239,8 @@ partial def updateTrailing {α} (trailing : Substring) : Syntax α → Syntax α
   if args.size == 0 then n
   else
    let i    := args.size - 1;
-   let last := updateTrailing (args.get i);
-   let args := args.set i last;
+   let last := updateTrailing (args.get! i);
+   let args := args.set! i last;
    Syntax.node k args
 | s => s
 
@@ -265,9 +265,9 @@ partial def getTailInfo {α} : Syntax α → Option SourceInfo
   if i == 0 then none
   else
     let i := i - 1;
-    let v := a.get i;
+    let v := a.get! i;
     match f v with
-    | some v => some $ a.set i v
+    | some v => some $ a.set! i v
     | none   => updateLast i
 
 partial def setTailInfoAux {α} (info : Option SourceInfo) : Syntax α → Option (Syntax α)
@@ -295,7 +295,7 @@ partial def reprint {α} : Syntax α → Option String
   if kind == choiceKind then
     if args.size == 0 then failure
     else do
-      s ← reprint (args.get 0);
+      s ← reprint (args.get! 0);
       args.mfoldlFrom (fun s stx => do s' ← reprint stx; guard (s == s'); pure s) s 1
   else args.mfoldl (fun r stx => do s ← reprint stx; pure $ r ++ s) ""
 | _ => ""
@@ -379,7 +379,7 @@ namespace Syntax
 def isStrLit {α} : Syntax α → Option String
 | Syntax.node k args   =>
   if k == strLitKind && args.size == 1 then
-    match args.get 0 with
+    match args.get! 0 with
     | (Syntax.atom _ val) => some val
     | _ => none
   else
@@ -448,7 +448,7 @@ else
 def isNatLitAux {α} (nodeKind : SyntaxNodeKind) : Syntax α → Option Nat
 | Syntax.node k args   =>
   if k == nodeKind && args.size == 1 then
-    match args.get 0 with
+    match args.get! 0 with
     | (Syntax.atom _ val) => decodeNatLitVal val
     | _ => none
   else
diff --git a/tests/bench/qsort.lean b/tests/bench/qsort.lean
index b7501cbfd8..57c88e3397 100644
--- a/tests/bench/qsort.lean
+++ b/tests/bench/qsort.lean
@@ -10,7 +10,7 @@ def mkRandomArray : Nat → Elem → Array Elem → Array Elem
 partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
 | i =>
   if i < a.size - 1 then do
-    unless (a.get i <= a.get (i+1)) $ throw (IO.userError "array is not sorted");
+    unless (a.get! i <= a.get! (i+1)) $ throw (IO.userError "array is not sorted");
     checkSortedAux (i+1)
   else
     pure ()
@@ -23,21 +23,21 @@ prefix `↑`:max := coe
 @[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : α → α → Bool) (hi : Idx) (pivot : α) : Array α → Idx → Idx → Idx × Array α
 | as, i, j =>
   if j < hi then
-    if lt (as.get ↑j) pivot then
-      let as := as.swap ↑i ↑j;
+    if lt (as.get! ↑j) pivot then
+      let as := as.swap! ↑i ↑j;
       partitionAux as (i+1) (j+1)
     else
       partitionAux as i (j+1)
   else
-    let as := as.swap ↑i ↑hi;
+    let as := as.swap! ↑i ↑hi;
     (i, as)
 
 @[inline] def partition {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (lo hi : Idx) : Idx × Array α :=
 let mid := (lo + hi) / 2;
-let as  := if lt (as.get ↑mid) (as.get ↑lo) then as.swap ↑lo ↑mid else as;
-let as  := if lt (as.get ↑hi)  (as.get ↑lo) then as.swap ↑lo ↑hi  else as;
-let as  := if lt (as.get ↑mid) (as.get ↑hi) then as.swap ↑mid ↑hi else as;
-let pivot := as.get ↑hi;
+let as  := if lt (as.get! ↑mid) (as.get! ↑lo) then as.swap! ↑lo ↑mid else as;
+let as  := if lt (as.get! ↑hi)  (as.get! ↑lo) then as.swap! ↑lo ↑hi  else as;
+let as  := if lt (as.get! ↑mid) (as.get! ↑hi) then as.swap! ↑mid ↑hi else as;
+let pivot := as.get! ↑hi;
 partitionAux lt hi pivot as lo lo
 
 @[specialize] partial def qsortAux {α : Type} [Inhabited α] (lt : α → α → Bool) : Array α → Idx → Idx → Array α
diff --git a/tests/bench/unionfind.lean b/tests/bench/unionfind.lean
index df4275b5b4..8ce07c866a 100644
--- a/tests/bench/unionfind.lean
+++ b/tests/bench/unionfind.lean
@@ -47,10 +47,10 @@ def findEntryAux : Nat → Node → M nodeData
 | i+1, n =>
   do s ← read;
      if h : n < s.size then
-       do { let e := s.fget ⟨n, h⟩;
+       do { let e := s.get ⟨n, h⟩;
             if e.find = n then pure e
             else do e₁ ← findEntryAux i e.find;
-                    updt (fun s => s.set n e₁);
+                    updt (fun s => s.set! n e₁);
                     pure e₁ }
      else error "invalid Node"
 
@@ -71,11 +71,11 @@ do r₁ ← findEntry n₁;
    r₂ ← findEntry n₂;
    if r₁.find = r₂.find then pure ()
    else updt $ fun s =>
-     if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find }
+     if r₁.rank < r₂.rank then s.set! r₁.find { find := r₂.find }
      else if r₁.rank = r₂.rank then
-        let s₁ := s.set r₁.find { find := r₂.find };
-        s₁.set r₂.find { rank := r₂.rank + 1, .. r₂}
-     else s.set r₂.find { find := r₁.find }
+        let s₁ := s.set! r₁.find { find := r₂.find };
+        s₁.set! r₂.find { rank := r₂.rank + 1, .. r₂}
+     else s.set! r₂.find { find := r₁.find }
 
 
 def mkNodes : Nat → M Unit
diff --git a/tests/compiler/bytearray_bug.lean b/tests/compiler/bytearray_bug.lean
index 421a7df880..d200af09b8 100644
--- a/tests/compiler/bytearray_bug.lean
+++ b/tests/compiler/bytearray_bug.lean
@@ -1,4 +1,4 @@
 def main (xs : List String) : IO Unit :=
   let arr := (let e := ByteArray.empty; e.push (UInt8.ofNat 10));
-  let v := arr.data.get 0;
+  let v := arr.data.get! 0;
   IO.println v
diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean
index 9864da4577..035b37ef08 100644
--- a/tests/compiler/phashmap.lean
+++ b/tests/compiler/phashmap.lean
@@ -8,15 +8,15 @@ partial def formatMap : Node Nat Nat → Format
 | Node.collision keys vals _   => Format.sbracket $
   keys.size.fold
     (fun i fmt =>
-      let k := keys.get i;
-      let v := vals.get i;
+      let k := keys.get! i;
+      let v := vals.get! i;
       let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
       p ++ "c@" ++ Format.paren (format k ++ " => " ++ format v))
     Format.nil
 | Node.entries entries        => Format.sbracket $
   entries.size.fold
     (fun i fmt =>
-      let entry := entries.get i;
+      let entry := entries.get! i;
       let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
       p ++
       match entry with
diff --git a/tests/compiler/phashmap2.lean b/tests/compiler/phashmap2.lean
index 7f1bd20aa6..fc032e84a6 100644
--- a/tests/compiler/phashmap2.lean
+++ b/tests/compiler/phashmap2.lean
@@ -8,15 +8,15 @@ partial def formatMap : Node Nat Nat → Format
 | Node.collision keys vals _   => Format.sbracket $
   keys.size.fold
     (fun i fmt =>
-      let k := keys.get i;
-      let v := vals.get i;
+      let k := keys.get! i;
+      let v := vals.get! i;
       let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
       p ++ "c@" ++ Format.paren (format k ++ " => " ++ format v))
     Format.nil
 | Node.entries entries        => Format.sbracket $
   entries.size.fold
     (fun i fmt =>
-      let entry := entries.get i;
+      let entry := entries.get! i;
       let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
       p ++
       match entry with
diff --git a/tests/compiler/phashmap3.lean b/tests/compiler/phashmap3.lean
index 5e043d7b3e..594783e064 100644
--- a/tests/compiler/phashmap3.lean
+++ b/tests/compiler/phashmap3.lean
@@ -8,15 +8,15 @@ partial def formatMap : Node Nat Nat → Format
 | Node.collision keys vals _   => Format.sbracket $
   keys.size.fold
     (fun i fmt =>
-      let k := keys.get i;
-      let v := vals.get i;
+      let k := keys.get! i;
+      let v := vals.get! i;
       let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
       p ++ "c@" ++ Format.paren (format k ++ " => " ++ format v))
     Format.nil
 | Node.entries entries        => Format.sbracket $
   entries.size.fold
     (fun i fmt =>
-      let entry := entries.get i;
+      let entry := entries.get! i;
       let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
       p ++
       match entry with
diff --git a/tests/lean/bytearray.lean b/tests/lean/bytearray.lean
index eb60013637..99b2cd680a 100644
--- a/tests/lean/bytearray.lean
+++ b/tests/lean/bytearray.lean
@@ -3,9 +3,9 @@ do
 let bs := [1, 2, 3].toByteArray;
 IO.println bs;
 let bs := bs.push 4;
-let bs := bs.set 1 20;
+let bs := bs.set! 1 20;
 IO.println bs;
-let bs₁ := bs.set 2 30;
+let bs₁ := bs.set! 2 30;
 IO.println bs₁;
 IO.println bs;
 IO.println bs.size;
diff --git a/tests/lean/ref1.lean b/tests/lean/ref1.lean
index eba3cec526..809b3333ae 100644
--- a/tests/lean/ref1.lean
+++ b/tests/lean/ref1.lean
@@ -9,7 +9,7 @@ n.mfor $ fun i => do
 
 def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit :=
 do a ← r.swap ∅;
-   a.size.mfor (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get i)));
+   a.size.mfor (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
    r.swap a;
    pure ()
 
diff --git a/tests/lean/repr_issue.lean b/tests/lean/repr_issue.lean
index 29d2d32d37..1e515b5770 100644
--- a/tests/lean/repr_issue.lean
+++ b/tests/lean/repr_issue.lean
@@ -1,7 +1,7 @@
 def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
-catch (do modify $ fun (a : Array Nat) => a.set 0 33;
+catch (do modify $ fun (a : Array Nat) => a.set! 0 33;
           throw "error")
-      (fun _ => do a ← get; pure $ a.get 0)
+      (fun _ => do a ← get; pure $ a.get! 0)
 
 def ex₁ : StateT (Array Nat) (ExceptT String Id) Nat :=
 foo