toki/numidr
1
0
Fork 0
Code Issues Pull requests Activity

Remove unnecessary totality asserts

Browse source
This commit is contained in:
Kiana Sheibani 2022-05-11 23:40:59 -04:00
parent 562d501f33
commit 0a4be10a0d
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Data/NumIdr/PrimArray.idr
View file

@ -48,7 +48,7 @@ unsafeIndex n arr = unsafePerformIO $ arrayDataGet n $ content arr
export export
index : Nat -> PrimArray a -> Maybe a index : Nat -> PrimArray a -> Maybe a
index n arr = if n < length arr index n arr = if n < length arr
then Just $ assert_total $ unsafeIndex n arr then Just $ unsafeIndex n arr
else Nothing else Nothing
@ -59,7 +59,7 @@ toList arr = iter (length arr) []
iter : Nat -> List a -> List a iter : Nat -> List a -> List a
iter Z acc = acc iter Z acc = acc
iter (S n) acc = let el = unsafeIndex n arr iter (S n) acc = let el = unsafeIndex n arr
in assert_total $ iter n (el :: acc) in iter n (el :: acc)
export export
fromList : List a -> PrimArray a fromList : List a -> PrimArray a