diff --git a/tests/lean/grind/bool.lean b/tests/lean/grind/bool.lean new file mode 100644 index 0000000000..c7c9cac459 --- /dev/null +++ b/tests/lean/grind/bool.lean @@ -0,0 +1,8 @@ +reset_grind_attrs% + +example [BEq α] (a b : α) : (a == b && a == b) = (a == b) := by + rw [Bool.eq_iff_iff] + grind -- succeeds + +example [BEq α] (a b : α) : (a == b && a == b) = (a == b) := by + grind -- fails