@@ -55,7 +55,7 @@ natToFin (S k) (S j) with (natToFin k j)
55natToFin _ _ = Nothing
55natToFin _ _ = Nothing
57integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
57integerToFin : 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
60data IsJust : Maybe a -> Type where
60data IsJust : Maybe a -> Type where
61 ItIsJust : IsJust {a} (Just x)
61 ItIsJust : IsJust {a} (Just x)