max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: test for Int.mod bug

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-31 08:57:41 -08:00
parent c4cfbceb71
commit 60805b5c0c
2 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
tests/lean/intModBug.lean Normal file
View file

@ -0,0 +1,9 @@
#reduce (10 : Int) % 0
#reduce (-10 : Int) % 0
#eval (10:Int) % 0
#eval (-10 : Int) % 0
#reduce (10000000000000000000000000000000000 : Int) % 0
#reduce (-10000000000000000000000000000000000 : Int) % 0
#eval (10000000000000000000000000000000000:Int) % 0
#eval (-10000000000000000000000000000000000 : Int) % 0

8
tests/lean/intModBug.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
Int.ofNat 10
Int.negSucc 9
10
9
Int.ofNat 10000000000000000000000000000000000
Int.negSucc 9999999999999999999999999999999999
10000000000000000000000000000000000
9999999999999999999999999999999999