Commit 2024-04-24 00:10 b331c4b0

View on Github →

chore(Init): add deprecation dates; remove long-deprecated items (#12347) All removed items are virtually unused in mathlib and have been deprecated for over a year.

Estimated changes

Modified Mathlib/Init/Core.lean

deleted inductive BinTree

deleted def Std.Prec.arrow

deleted def Std.Prec.max

deleted def Std.Prec.maxPlus

deleted def Std.Priority.default

deleted def Std.Priority.max

Modified Mathlib/Init/Data/List/Basic.lean

deleted def List.findIndex

Modified Mathlib/Init/Logic.lean

deleted theorem Decidable.not_or_iff_and_not

deleted theorem Implies.trans

deleted def Implies

deleted def NonContradictory

deleted theorem and_assoc'

deleted theorem and_comm'

deleted theorem if_t_t

deleted theorem or_assoc'

deleted theorem or_comm'

deleted theorem trans_rel_left

deleted theorem trans_rel_right

Modified Mathlib/RingTheory/Int/Basic.lean

Modified scripts/nolints.json

Modified scripts/noshake.json