adjust test

Author: Rob23oba

tests/lean/run/compiler_bug_neutral.lean

@@ -0,0 +1,26 @@
+/-!
+This test guards against a constant folding bug
+-/
+
+
+def danger : UInt64 := UInt64.ofNat UInt64.size - 1
+theorem danger_eq_large : danger = 18446744073709551615 := by decide +kernel
+/--
+error: Tactic `native_decide` evaluated that the proposition
+  danger = 1
+is false
+-/
+#guard_msgs in
+theorem danger_eq_one : danger = 1 := by native_decide
+theorem bad : False := by simpa using danger_eq_large.symm.trans danger_eq_one
+
+def danger2 (x : Nat) : Nat := 0 - x
+theorem danger2_eq_zero : danger2 1 = 0 := by decide +kernel
+/--
+error: Tactic `native_decide` evaluated that the proposition
+  danger2 1 = 1
+is false
+-/
+#guard_msgs in
+theorem danger2_eq_one : danger2 1 = 1 := by native_decide
+theorem bad2 : False := by simpa using danger2_eq_zero.symm.trans danger2_eq_one