From 475c7e18cd8f075d221b0a91f3fcff80f28839f9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 10 Jul 2022 14:53:22 -0700
Subject: [PATCH] chore: missing `GetElem` instances

---
 src/Init/Data/Array/Basic.lean      | 2 +-
 src/Init/Data/ByteArray/Basic.lean  | 5 ++++-
 src/Init/Data/FloatArray/Basic.lean | 5 ++++-
 3 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 98c85c9afb..f260604112 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -41,7 +41,7 @@ def singleton (v : α) : Array α :=
 def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
   a[i.toNat]
 
-instance : GetElem (Array α) USize α fun xs i => LT.lt i.toNat xs.size where
+instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
 def back [Inhabited α] (a : Array α) : α :=
diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean
index 45e058c5ad..4c7f861c68 100644
--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@@ -49,9 +49,12 @@ def get! : (@& ByteArray) → (@& Nat) → UInt8
 def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
   | ⟨bs⟩, i => bs.get i
 
-instance : GetElem ByteArray Nat UInt8 fun xs i => LT.lt i xs.size where
+instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
+  getElem xs i h := xs.uget 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 e98af22291..b35f2a38ee 100644
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@@ -55,9 +55,12 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
   else
     none
 
-instance : GetElem FloatArray Nat Float fun xs i => LT.lt i xs.size where
+instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
+  getElem xs i h := xs.uget 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⟩