Bug fix in integerToFin.
Previously, integerToFin returned (Just fZ) for negative integers. Now
it returns Nothing.
commitadea8a9e481dbe67d72e34d23cada6875c920fc5
authorEric Walkingshaw <eric@walkingshaw.net>
dateMon 25 Nov 2013, 18:23 (13 years ago)
parent6aeaeb6
libs/prelude/Prelude/Fin.idr+1−1
@@ -55,7 +55,7 @@ natToFin (S k) (S j) with (natToFin k j)
5555natToFin _ _ = Nothing
5656
5757integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
58−integerToFin x = natToFin (cast x)
58+integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
5959
6060data IsJust : Maybe a -> Type where
6161 ItIsJust : IsJust {a} (Just x)