Commit 2022-10-01 22:27 56b19bde

View on Github →

chore: update lean + std4 09-30 (#448)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Rename.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/Cases.lean

modified def Lean.Parser.Tactic.ElimApp.evalNames

Modified Mathlib/Tactic/Conv.lean

Deleted Mathlib/Tactic/DSimp.lean

deleted def Mathlib.Tactic.Conv.evalDSimp

Modified Mathlib/Tactic/Find.lean

Modified Mathlib/Tactic/HelpCmd.lean

Modified Mathlib/Tactic/Recover.lean

added def Lean.HashSet.insertMany

deleted def Std.HashSet.insertMany

Modified Mathlib/Util/Export.lean

Modified Mathlib/Util/MemoFix.lean

Modified Mathlib/Util/Simp.lean

added def Lean.PHashSet.toList

deleted def Std.PHashSet.toList

Modified lean-toolchain

Modified lean_packages/manifest.json

Modified scripts/nolints.json

Deleted test/DSimp.lean

Modified test/Have.lean