From 603f2dee73de3078fd88f12de2f311e5a5c144ce Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Sep 2020 13:15:57 -0700
Subject: [PATCH] fix: unnecessary `get!`

---
 src/Init/Data/FloatArray/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean
index 5056e9f54e..8840cd937d 100644
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@@ -63,8 +63,8 @@ s.size == 0
 
 partial def toListAux (ds : FloatArray) : Nat → List Float → List Float
 | i, r =>
-  if i < ds.size then
-    toListAux (i+1) (ds.get! i :: r)
+  if h : i < ds.size then
+    toListAux (i+1) (ds.get ⟨i, h⟩ :: r)
   else
     r.reverse