Merge pull request #670 from walkie/master
Minor bug fix in Prelude.Fin.integerToFin.
commit16847d5f36991a88b7aac6dcef30aeff9fc17d04
authorEdwin Brady <edwin.brady@gmail.com>
dateMon 25 Nov 2013, 11:11 (13 years ago)
parent4f1b604adea8a9
.gitignore+2
@@ -1,5 +1,7 @@
11dist
22cabal-dev/
3+.cabal-sandbox
4+cabal.sandbox.config
35*.ibc
46*.o
57*.a
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)