From 5ba171d9460ba9a152c33e0575755f1c6cbb68f0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 7 Mar 2021 13:09:23 -0800 Subject: [PATCH] test: for `Int.negSucc` bug --- tests/lean/intNegSucc.lean | 16 ++++++++++++++++ tests/lean/intNegSucc.lean.expected.out | 14 ++++++++++++++ 2 files changed, 30 insertions(+) create mode 100644 tests/lean/intNegSucc.lean create mode 100644 tests/lean/intNegSucc.lean.expected.out diff --git a/tests/lean/intNegSucc.lean b/tests/lean/intNegSucc.lean new file mode 100644 index 0000000000..d9e9089290 --- /dev/null +++ b/tests/lean/intNegSucc.lean @@ -0,0 +1,16 @@ +def Int64Min : Int := -1*(Int.ofNat ((UInt64.size / 2))) + +#eval Int.negSucc 9223372036854775807 +#reduce Int.negSucc 9223372036854775807 +#print "---" +#eval - Int.negSucc 9223372036854775807 +#reduce - Int.negSucc 9223372036854775807 +#print "---" +#eval Int.negSucc 9223372036854775807 == 0 +#reduce Int.negSucc 9223372036854775807 == 0 +#print "---" +#eval Int.negSucc 9223372036854775807 == Int64Min +#reduce Int.negSucc 9223372036854775807 == Int64Min +#print "---" +#eval (Int.negSucc 9223372036854775807) + 1 == 1 +#reduce (Int.negSucc 9223372036854775807) + 1 == 1 diff --git a/tests/lean/intNegSucc.lean.expected.out b/tests/lean/intNegSucc.lean.expected.out new file mode 100644 index 0000000000..64be973318 --- /dev/null +++ b/tests/lean/intNegSucc.lean.expected.out @@ -0,0 +1,14 @@ +-9223372036854775808 +Int.negSucc 9223372036854775807 +--- +9223372036854775808 +Int.ofNat 9223372036854775808 +--- +false +false +--- +true +true +--- +false +false