From 36ebccb822ec6b072fafacd07508ac5ffb1bca83 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 9 Jul 2022 15:59:44 -0700
Subject: [PATCH] chore: fix tests

---
 src/Init/Data/ByteArray/Basic.lean  |  3 +++
 src/Init/Data/FloatArray/Basic.lean |  3 +++
 tests/lean/986.lean.expected.out    |  2 +-
 tests/lean/run/arthur1.lean         |  2 +-
 tests/lean/run/getOp.lean           | 22 ----------------------
 tests/lean/run/sarray.lean          |  2 +-
 6 files changed, 9 insertions(+), 25 deletions(-)
 delete mode 100644 tests/lean/run/getOp.lean

diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean
index f8dcc55366..534007331a 100644
--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@@ -52,6 +52,9 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 @[inline] def getOp (self : ByteArray) (idx : Nat) : UInt8 :=
   self.get! idx
 
+instance : GetElem ByteArray Nat UInt8 fun xs i => LT.lt i xs.size where
+  getElem xs i h := xs.get ⟨i, h⟩
+
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean
index f9b5a1b9bd..4864f74952 100644
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@@ -58,6 +58,9 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 @[inline] def getOp (self : FloatArray) (idx : Nat) : Float :=
   self.get! idx
 
+instance : GetElem FloatArray Nat Float fun xs i => LT.lt i xs.size where
+  getElem xs i h := xs.get ⟨i, h⟩
+
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩
diff --git a/tests/lean/986.lean.expected.out b/tests/lean/986.lean.expected.out
index 9bfbb50854..057d5226db 100644
--- a/tests/lean/986.lean.expected.out
+++ b/tests/lean/986.lean.expected.out
@@ -4,7 +4,7 @@
   (h : Nat.succ j' < Array.size a),
   Array.insertionSort.swapLoop lt a (Nat.succ j') h =
     let_fun h' := (_ : j' < Array.size a);
-    if lt (Array.getOp a { val := Nat.succ j', isLt := h }) (Array.getOp a { val := j', isLt := h' }) = true then
+    if lt (getElem a (Nat.succ j') h) (getElem a j' h') = true then
       Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j'
         (_ : j' < Array.size (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }))
     else a
diff --git a/tests/lean/run/arthur1.lean b/tests/lean/run/arthur1.lean
index f0d804e978..0377d316c0 100644
--- a/tests/lean/run/arthur1.lean
+++ b/tests/lean/run/arthur1.lean
@@ -366,7 +366,7 @@ def State.step : State → State
   | s@(done ..)  => s
 
 def Context.equiv (cₗ cᵣ : Context) : Prop :=
-  ∀ n, cₗ[n] = cᵣ[n]
+  ∀ n : String, cₗ[n] = cᵣ[n]
 
 def State.stepN : State → Nat → State
   | s, 0     => s
diff --git a/tests/lean/run/getOp.lean b/tests/lean/run/getOp.lean
deleted file mode 100644
index f018238b98..0000000000
--- a/tests/lean/run/getOp.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-def MyArray := Array
-
-namespace MyArray
-
-def getOp? (self : MyArray α) (idx : Nat) : Option α :=
-  Array.get? self idx
-
-def getOp! [Inhabited α] (self : MyArray α) (idx : Nat) : α :=
-  Array.get! self idx
-
-def getOp (self : MyArray α) (idx : Fin self.size) : α :=
-  Array.get self idx
-
-end MyArray
-
-variable (a : MyArray Nat)
-
-#check a[0]!
-#check a[0]?
-
-variable (i : Fin a.size)
-#check a[i]
diff --git a/tests/lean/run/sarray.lean b/tests/lean/run/sarray.lean
index 75061c6544..e835a729ea 100644
--- a/tests/lean/run/sarray.lean
+++ b/tests/lean/run/sarray.lean
@@ -26,7 +26,7 @@ def tst3 (n : Nat) (expected : UInt32) : IO Unit := do
   let bs := mkByteArray n
   let mut sum := 0
   for i in [:bs.size] do
-    sum := sum + bs[i].toUInt32
+    sum := sum + bs[i]!.toUInt32
   assert! sum == expected
   IO.println sum