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