Skip to content

Commit

Permalink
Bug fix: Bool.not_ne_self missing "()" (#1755)
Browse files Browse the repository at this point in the history
where `!b ≠ b` is interpreted as `(!decide (b ≠ b))`, but meant to be `(!b) ≠ b`.
  • Loading branch information
casavaca committed Jan 22, 2023
1 parent 02f4a7d commit 69d3684
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Bool/Basic.lean
Expand Up @@ -220,7 +220,7 @@ theorem ne_not {a b : Bool} : a ≠ !b ↔ a = b :=
theorem not_ne : ∀ {a b : Bool}, (!a) ≠ b ↔ a = b := not_not_eq
#align bool.bnot_ne Bool.not_ne

lemma not_ne_self : ∀ b : Bool, !b ≠ b := by decide
lemma not_ne_self : ∀ b : Bool, (!b) ≠ b := by decide
#align bool.bnot_ne_self Bool.not_ne_self

lemma self_ne_not : ∀ b : Bool, b ≠ !b := by decide
Expand Down

0 comments on commit 69d3684

Please sign in to comment.