Merge pull request #5 from leanprover-community/determ-tests

chore: make tests deterministic

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})