Commit 2024-06-11 03:54 8852c2c9

View on Github →

chore(Data/Bool/Basic): deprecate duplicate definitions (#13589) Deprecates theorems in favour of the versions in the Lean repository. This is actually pretty close to making Data.Bool.Basic a leaf file. We'd just need to move the LinearOrder instance elsewhere, and injective_iff.

Estimated changes

Modified Mathlib/Computability/RegularExpressions.lean

Modified Mathlib/Data/Bool/AllAny.lean

Modified Mathlib/Data/Bool/Basic.lean

deleted theorem Bool.coe_decide

deleted theorem Bool.decide_False

deleted theorem Bool.decide_True

deleted theorem Bool.decide_not

deleted theorem Bool.eq_false_of_ne_true

deleted theorem Bool.eq_iff_eq_true_iff

deleted theorem Bool.eq_true_of_ne_false

deleted theorem Bool.not_false'

deleted theorem Bool.not_ne

deleted theorem Bool.of_decide_iff

Modified Mathlib/Data/Bool/Set.lean

Modified Mathlib/Data/List/Perm.lean

Modified Mathlib/Data/Nat/Bitwise.lean

Modified Mathlib/Data/Num/Bitwise.lean

Modified Mathlib/Init/Data/Bool/Lemmas.lean

deleted theorem Bool.coe_and_iff

deleted theorem Bool.coe_or_iff

modified theorem Bool.decide_congr