From d03aaec9442afb32d3961dd5fb6eb8afdc399d71 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Oct 2021 16:00:11 -0700
Subject: [PATCH] feat: expose new float/byte array primitives

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

diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean
index 52437a6f88..783ba5c619 100644
--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@@ -33,14 +33,30 @@ def push : ByteArray → UInt8 → ByteArray
 def size : (@& ByteArray) → Nat
   | ⟨bs⟩ => bs.size
 
+@[extern "lean_byte_array_uget"]
+def uget : (a : @& ByteArray) → (i : USize) → i.toNat < a.size → UInt8
+  | ⟨bs⟩, i, h => bs.uget i h
+
 @[extern "lean_byte_array_get"]
 def get! : (@& ByteArray) → (@& Nat) → UInt8
   | ⟨bs⟩, i => bs.get! i
 
+@[extern "lean_byte_array_fget"]
+def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
+  | ⟨bs⟩, i => bs.get i
+
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
 
+@[extern "lean_byte_array_fset"]
+def set : (a : ByteArray) → (@& Fin a.size) → UInt8 → ByteArray
+  | ⟨bs⟩, i, b => ⟨bs.set i b⟩
+
+@[extern "lean_byte_array_uset"]
+def uset : (a : ByteArray) → (i : USize) → UInt8 → i.toNat < a.size → ByteArray
+  | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
+
 def isEmpty (s : ByteArray) : Bool :=
   s.size == 0
 
diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean
index 2c56cee764..f890e1c078 100644
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@@ -33,9 +33,12 @@ def push : FloatArray → Float → FloatArray
 def size : (@& FloatArray) → Nat
   | ⟨ds⟩ => ds.size
 
+@[extern "lean_float_array_uget"]
+def uget : (a : @& FloatArray) → (i : USize) → i.toNat < a.size → Float
+  | ⟨ds⟩, i, h => ds.uget i h
+
 @[extern "lean_float_array_fget"]
-def get (ds : @& FloatArray) (i : @& Fin ds.size) : Float :=
-  match ds, i with
+def get : (ds : @& FloatArray) → (@& Fin ds.size) → Float
   | ⟨ds⟩, i => ds.get i
 
 @[extern "lean_float_array_get"]
@@ -48,10 +51,13 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
   else
     none
 
+@[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⟩
+
 @[extern "lean_float_array_fset"]
-def set (ds : FloatArray) (i : @& Fin ds.size) (d : Float) : FloatArray :=
-  match ds, i with
-  | ⟨ds⟩, i=> ⟨ds.set i d⟩
+def set : (ds : FloatArray) → (@& Fin ds.size) → Float → FloatArray
+  | ⟨ds⟩, i, d => ⟨ds.set i d⟩
 
 @[extern "lean_float_array_set"]
 def set! : FloatArray → (@& Nat) → Float → FloatArray