added the import

ufmg-smite · Aug 28, 2023 · 23f2ee1 · 23f2ee1
1 parent 8035a9e
commit 23f2ee1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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]]