Skip to content
Merged
8 changes: 4 additions & 4 deletions Test/Tactic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ example (xs : List Int) (f : Int → Int) : xs.map f = xs := by
/--
info: Unable to find a counter-example
---
warning: declaration uses 'sorry'
warning: declaration uses `sorry`
-/
#guard_msgs in
example (a : Sum Nat Nat) : a = a := by
Expand All @@ -131,7 +131,7 @@ example (a : Sum Nat Nat) : a = a := by
/--
warning: Gave up after failing to generate values that fulfill the preconditions 100 times.
---
warning: declaration uses 'sorry'
warning: declaration uses `sorry`
-/
#guard_msgs in
example (a b : Sum Nat Nat) : a ≠ a → a = b := by
Expand All @@ -142,7 +142,7 @@ open Nat in
/--
info: Unable to find a counter-example
---
warning: declaration uses 'sorry'
warning: declaration uses `sorry`
-/
#guard_msgs in
theorem testBit_pred :
Expand All @@ -164,7 +164,7 @@ theorem type_u (α : Type u) (l : List α) : l = l ++ l := by
/--
info: Unable to find a counter-example
---
warning: declaration uses 'sorry'
warning: declaration uses `sorry`
-/
#guard_msgs in
theorem true_example_with_guard (a : Nat) (ha : 4 ≤ a) : a = a := by
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.27.0
leanprover/lean4:v4.28.0-rc1