Commit 2022-09-27 16:29 6ff78b46

View on Github →

chore: update lean + std4 09-26 (#443)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

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

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/Conv.lean

Modified Mathlib/Tactic/DSimp.lean

Modified Mathlib/Tactic/LibrarySearch.lean

Modified Mathlib/Tactic/NormCast/Tactic.lean

Modified Mathlib/Tactic/NormNum.lean

Modified Mathlib/Tactic/PushNeg.lean

Deleted Mathlib/Tactic/ShowTerm.lean

Modified Mathlib/Tactic/ToAdditive.lean

Deleted Mathlib/Tactic/TryThis.lean

deleted def Tactic.TryThis.addExactSuggestion

deleted def Tactic.TryThis.addSuggestion

deleted def Tactic.TryThis.addTermSuggestion

deleted def Tactic.TryThis.delabToRefinableSyntax

Modified Mathlib/Util/Simp.lean

Modified lean-toolchain

Modified lean_packages/manifest.json

Modified scripts/nolints.json

Modified scripts/runLinter.lean

Deleted test/showTerm.lean