Skip to content

Commit

Permalink
fix: correct for surprising precedence in Bool DeMorgan laws (#4987)
Browse files Browse the repository at this point in the history
The DeMorgan laws as stated were being parsed as an inequality
```lean
! ((a && b) = (!a || !b))
```
So, I added parenthesis to force the intended meaning of 
```lean
(!(a && b)) = (!a || !b)
```
  • Loading branch information
alexkeizer committed Jun 12, 2023
1 parent 54b7211 commit 43cb986
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Data/Bool/Basic.lean
Expand Up @@ -304,11 +304,11 @@ theorem xor_iff_ne : ∀ {x y : Bool}, xor x y = true ↔ x ≠ y := by decide
/-! ### De Morgan's laws for booleans-/

@[simp]
theorem not_and : ∀ a b : Bool, !(a && b) = (!a || !b) := by decide
theorem not_and : ∀ a b : Bool, (!(a && b)) = (!a || !b) := by decide
#align bool.bnot_band Bool.not_and

@[simp]
theorem not_or : ∀ a b : Bool, !(a || b) = (!a && !b) := by decide
theorem not_or : ∀ a b : Bool, (!(a || b)) = (!a && !b) := by decide
#align bool.bnot_bor Bool.not_or

theorem not_inj : ∀ {a b : Bool}, !a = !b → a = b := by decide
Expand Down

0 comments on commit 43cb986

Please sign in to comment.