diff --git a/Smt/Reconstruction/Rewrites/Tactic.lean b/Smt/Reconstruction/Rewrites/Tactic.lean index f35a5187..004be8b9 100644 --- a/Smt/Reconstruction/Rewrites/Tactic.lean +++ b/Smt/Reconstruction/Rewrites/Tactic.lean @@ -91,5 +91,5 @@ example : (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ y2 ∨ b ∨ z1 ∨ z2 ∨ False) = example : (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ b ∧ z1 ∧ z2 ∧ True) = (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ z1 ∧ z2 ∧ True) := by smt_rw and bool_and_dup [[x1, x2, x3], [y1, y2], [z1, z2]] -example : (x1 ∨ x2 ∨ x3 ∨ (b ∨ y1 ∨ False) ∨ z1 ∨ False) = (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ z1 ∨ False) := by +example : (x1 ∨ x2 ∨ x3 ∨ (b ∨ y1 ∨ False) ∨ z1 ∨ False)= (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ z1 ∨ False) := by smt_rw or bool_or_flatten [[x1, x2, x3], [b], [y1], [z1]]