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