idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 01:01:59 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #3267 from stefan-hoeck/fin0

Browse Source 
[ fix ] issue 3266
This commit is contained in:
André Videla 2024-04-23 00:50:10 +09:00 committed by GitHub
commit 2298f8837b
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
libs/base/Data/Fin.idr
View File

@ -230,8 +230,9 @@ finFromInteger x = natToFinLt (fromInteger x)
-- even when the function is unused (issue #2032)
public export
integerLessThanNat : Integer -> Nat -> Bool
integerLessThanNat 0 (S m) = True
integerLessThanNat x n with (x < the Integer 0)
integerLessThanNat _ _ | True = True -- if `x < 0` then `x < n` for any `n : Nat`
integerLessThanNat _ _ | True = False -- don't support negative literals
integerLessThanNat x (S m) | False = integerLessThanNat (x-1) m -- recursive case
integerLessThanNat x Z | False = False -- `x >= 0` contradicts `x < Z`

5
tests/base/data_fin/fromInteger.idr
View File

@ -20,3 +20,8 @@ eq1 = Refl
-- and anybody measures the time it takes this test to run...
addFourMillion : Int -> Int
addFourMillion x = 4000000 + x
-- issue #3266
failing
fin0 : Fin 0
fin0 = (-1)