Commit 2024-01-30 01:07 d3a6c9f3

View on Github →

chore: bump Std to leanprover/std4#242 (#10104)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Sign.lean

Modified Mathlib/Mathport/Notation.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Common.lean

Modified Mathlib/Tactic/Observe.lean

Modified Mathlib/Tactic/Propose.lean

Modified Mathlib/Tactic/RewriteSearch.lean

Modified Mathlib/Tactic/Rewrites.lean

Deleted Mathlib/Tactic/TryThis.lean

deleted def addHaveSuggestion

deleted def addRewriteSuggestion

Deleted Mathlib/Util/Syntax.lean

deleted def Lean.Syntax.TSepArray.ofElems

deleted def Lean.TSyntax.replaceM

Modified lake-manifest.json

Modified test/LibrarySearch/basic.lean

Modified test/RewriteSearch/Polynomial.lean

Modified test/propose.lean

Modified test/solve_by_elim/basic.lean