Skip to content

Commit

Permalink
fix: Data.Bool.Basic fix statement of not_inj (#5688)
Browse files Browse the repository at this point in the history
Due to the precedence of not, the statement was `!decide (a = !b) -> a = b`. Now it is the correct statement
  • Loading branch information
ChrisHughes24 committed Jul 3, 2023
1 parent ae5e808 commit a1e1e2f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Bool/Basic.lean
Expand Up @@ -311,7 +311,7 @@ theorem not_and : ∀ 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
theorem not_inj : ∀ {a b : Bool}, (!a) = !b → a = b := by decide
#align bool.bnot_inj Bool.not_inj

-- Porting note: having to unfold here is not pretty.
Expand Down

0 comments on commit a1e1e2f

Please sign in to comment.