Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-05-07 06:40
5e843131
View on Github →
chore: update Std -> Batteries (
#12720
)
Estimated changes
Modified
LongestPole/Main.lean
Modified
Mathlib/Algebra/BigOperators/Basic.lean
Modified
Mathlib/Algebra/BigOperators/Finprod.lean
Modified
Mathlib/Algebra/DirectSum/Basic.lean
Modified
Mathlib/Algebra/HierarchyDesign.lean
Modified
Mathlib/Algebra/Order/Ring/WithTop.lean
Modified
Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean
Modified
Mathlib/Control/Functor.lean
Modified
Mathlib/Data/Array/Basic.lean
Modified
Mathlib/Data/Array/ExtractLemmas.lean
Modified
Mathlib/Data/BinaryHeap.lean
Modified
Mathlib/Data/BitVec/Defs.lean
Modified
Mathlib/Data/DList/Basic.lean
added
def
Batteries.DList.join
added
theorem
Batteries.DList_lazy
added
theorem
Batteries.DList_singleton
deleted
def
Std.DList.join
deleted
theorem
Std.DList_lazy
deleted
theorem
Std.DList_singleton
Modified
Mathlib/Data/DList/Defs.lean
added
def
Batteries.DList.lazy_ofList
added
theorem
Batteries.DList.ofList_toList
added
theorem
Batteries.DList.toList_append
added
theorem
Batteries.DList.toList_cons
added
theorem
Batteries.DList.toList_empty
added
theorem
Batteries.DList.toList_ofList
added
theorem
Batteries.DList.toList_push
added
theorem
Batteries.DList.toList_singleton
deleted
def
Std.DList.lazy_ofList
deleted
theorem
Std.DList.ofList_toList
deleted
theorem
Std.DList.toList_append
deleted
theorem
Std.DList.toList_cons
deleted
theorem
Std.DList.toList_empty
deleted
theorem
Std.DList.toList_ofList
deleted
theorem
Std.DList.toList_push
deleted
theorem
Std.DList.toList_singleton
Modified
Mathlib/Data/DList/Instances.lean
added
def
Batteries.DList.listEquivDList
deleted
def
Std.DList.listEquivDList
Modified
Mathlib/Data/Fin/Basic.lean
Modified
Mathlib/Data/Fintype/Basic.lean
Modified
Mathlib/Data/HashMap.lean
added
def
Batteries.HashMap.consVal
added
def
Batteries.HashMap.keys
added
def
Batteries.HashMap.values
added
def
Batteries.RBSet.insertList
deleted
def
Std.HashMap.consVal
deleted
def
Std.HashMap.keys
deleted
def
Std.HashMap.values
deleted
def
Std.RBSet.insertList
Modified
Mathlib/Data/Int/ModEq.lean
Modified
Mathlib/Data/LazyList/Basic.lean
Modified
Mathlib/Data/List/Basic.lean
Modified
Mathlib/Data/List/Defs.lean
Modified
Mathlib/Data/List/EditDistance/Defs.lean
Modified
Mathlib/Data/List/TFAE.lean
Modified
Mathlib/Data/MLList/BestFirst.lean
Modified
Mathlib/Data/MLList/Dedup.lean
Modified
Mathlib/Data/MLList/DepthFirst.lean
Modified
Mathlib/Data/MLList/IO.lean
Modified
Mathlib/Data/MLList/Split.lean
Modified
Mathlib/Data/Rat/Init.lean
Modified
Mathlib/Data/Rbtree/Init.lean
Modified
Mathlib/Data/Seq/Seq.lean
Modified
Mathlib/Data/Seq/WSeq.lean
Modified
Mathlib/Data/String/Defs.lean
Modified
Mathlib/Data/Tree.lean
Modified
Mathlib/Data/UnionFind.lean
Modified
Mathlib/Data/Vector.lean
Modified
Mathlib/Init/Align.lean
Modified
Mathlib/Init/Classes/Order.lean
Modified
Mathlib/Init/Data/Bool/Basic.lean
Modified
Mathlib/Init/Data/Int/Basic.lean
Modified
Mathlib/Init/Data/Int/DivMod.lean
Modified
Mathlib/Init/Data/Int/Lemmas.lean
Modified
Mathlib/Init/Data/List/Basic.lean
Modified
Mathlib/Init/Data/List/Instances.lean
Modified
Mathlib/Init/Data/List/Lemmas.lean
Modified
Mathlib/Init/Data/Nat/GCD.lean
Modified
Mathlib/Init/Data/Nat/Lemmas.lean
Modified
Mathlib/Init/Data/Option/Lemmas.lean
Modified
Mathlib/Init/Data/Quot.lean
Modified
Mathlib/Init/Data/Rat/Basic.lean
Modified
Mathlib/Init/Order/Defs.lean
Modified
Mathlib/Init/Set.lean
Modified
Mathlib/Lean/Expr/Basic.lean
Modified
Mathlib/Lean/Meta.lean
Modified
Mathlib/Lean/Meta/Simp.lean
Modified
Mathlib/Lean/Name.lean
modified
def
allNamesByModule
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/Mathport/Notation.lean
Modified
Mathlib/Mathport/Syntax.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction.lean
Modified
Mathlib/Order/SetNotation.lean
Modified
Mathlib/Tactic/ApplyCongr.lean
Modified
Mathlib/Tactic/Attr/Core.lean
Modified
Mathlib/Tactic/Basic.lean
Modified
Mathlib/Tactic/CC/Datatypes.lean
Modified
Mathlib/Tactic/Cases.lean
Modified
Mathlib/Tactic/CategoryTheory/Elementwise.lean
Modified
Mathlib/Tactic/Core.lean
Modified
Mathlib/Tactic/Eqns.lean
Modified
Mathlib/Tactic/Explode.lean
Modified
Mathlib/Tactic/ExtractGoal.lean
Modified
Mathlib/Tactic/Find.lean
Modified
Mathlib/Tactic/FunProp/Core.lean
Modified
Mathlib/Tactic/FunProp/FunctionData.lean
Modified
Mathlib/Tactic/FunProp/RefinedDiscrTree.lean
Modified
Mathlib/Tactic/FunProp/Theorems.lean
Modified
Mathlib/Tactic/FunProp/Types.lean
Modified
Mathlib/Tactic/GCongr/Core.lean
Modified
Mathlib/Tactic/GCongr/ForwardAttr.lean
Modified
Mathlib/Tactic/Hint.lean
Modified
Mathlib/Tactic/Linarith/Datatypes.lean
Modified
Mathlib/Tactic/Linarith/Elimination.lean
Modified
Mathlib/Tactic/Linarith/Frontend.lean
Modified
Mathlib/Tactic/Linarith/Lemmas.lean
Modified
Mathlib/Tactic/Linarith/Parsing.lean
Modified
Mathlib/Tactic/Linarith/Preprocessing.lean
Modified
Mathlib/Tactic/Lint.lean
modified
def
Std.Tactic.Lint.structureInType
Modified
Mathlib/Tactic/NormNum/Core.lean
Modified
Mathlib/Tactic/Propose.lean
Modified
Mathlib/Tactic/Recall.lean
Modified
Mathlib/Tactic/Sat/FromLRAT.lean
Modified
Mathlib/Tactic/Says.lean
Modified
Mathlib/Tactic/Simps/Basic.lean
Modified
Mathlib/Tactic/Simps/NotationClass.lean
Modified
Mathlib/Tactic/Tauto.lean
Modified
Mathlib/Tactic/ToAdditive.lean
Modified
Mathlib/Tactic/Use.lean
Modified
Mathlib/Tactic/Widget/Calc.lean
Modified
Mathlib/Tactic/Widget/Conv.lean
Modified
Mathlib/Testing/SlimCheck/Functions.lean
Modified
Mathlib/Util/DischargerAsTactic.lean
Modified
Mathlib/Util/LongNames.lean
modified
def
printNameHashMap
Modified
Mathlib/Util/Superscript.lean
Modified
Mathlib/Util/WhatsNew.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
scripts/checkYaml.lean
Modified
scripts/noshake.json
Modified
test/Clean.lean
Modified
test/MLList.lean
Modified
test/MkIffOfInductive.lean
Modified
test/choose.lean
Modified
test/lift.lean
Modified
test/propose.lean
Modified
test/solve_by_elim/basic.lean
Modified
test/trans.lean