From 0a4be10a0d89dc8f26d3b118c8d8f21bd4aabd03 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Wed, 11 May 2022 23:40:59 -0400 Subject: [PATCH] Remove unnecessary totality asserts --- src/Data/NumIdr/PrimArray.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/NumIdr/PrimArray.idr b/src/Data/NumIdr/PrimArray.idr index 6aee6b5..f524462 100644 --- a/src/Data/NumIdr/PrimArray.idr +++ b/src/Data/NumIdr/PrimArray.idr @@ -48,7 +48,7 @@ unsafeIndex n arr = unsafePerformIO $ arrayDataGet n $ content arr export index : Nat -> PrimArray a -> Maybe a index n arr = if n < length arr - then Just $ assert_total $ unsafeIndex n arr + then Just $ unsafeIndex n arr else Nothing @@ -59,7 +59,7 @@ toList arr = iter (length arr) [] iter : Nat -> List a -> List a iter Z acc = acc iter (S n) acc = let el = unsafeIndex n arr - in assert_total $ iter n (el :: acc) + in iter n (el :: acc) export fromList : List a -> PrimArray a