From 64a9e5b3dac809dd66d203d5b22fe650d98ea2a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 4 Nov 2024 09:26:37 +0100
Subject: [PATCH] chore: make tests deterministi-- c

---
 Test/Tactic.lean | 37 +++++++++----------------------------
 1 file changed, 9 insertions(+), 28 deletions(-)

diff --git a/Test/Tactic.lean b/Test/Tactic.lean
index d86e45c..af3c257 100644
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@@ -150,31 +150,12 @@ theorem testBit_pred :
       (Bool.xor ((List.range i).all fun j => ! testBit x j) (testBit x i))) := by
   plausible
 
--- FIXME: the following two tests have become non-deterministic.
-
--- /--
--- error:
--- ===================
--- Found a counter-example!
--- f := 1
--- issue: ULift.up 1 = ULift.up 0 does not hold
--- (1 shrinks)
--- -------------------
--- -/
--- #guard_msgs in
--- theorem ulift_nat (f : ULift.{1} Nat) : f = ⟨0⟩ := by
---   plausible
-
--- /--
--- error:
--- ===================
--- Found a counter-example!
--- α := "ULift Int"
--- l := [0]
--- issue: [ULift.up 0] = [ULift.up 0, ULift.up 0] does not hold
--- (1 shrinks)
--- -------------------
--- -/
--- #guard_msgs in
--- theorem type_u (α : Type u) (l : List α) : l = l ++ l := by
---   plausible
+/-- error: Found a counter-example! -/
+#guard_msgs in
+theorem ulift_nat (f : ULift.{1} Nat) : f = ⟨0⟩ := by
+  plausible (config := {quiet := true})
+
+/-- error: Found a counter-example! -/
+#guard_msgs in
+theorem type_u (α : Type u) (l : List α) : l = l ++ l := by
+  plausible (config := {quiet := true})