Commit 2023-11-02 13:03 1400397d

View on Github →

chore: bump Std to Std#254 (#8106)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Lean/Meta/DiscrTree.lean

deleted def Lean.Meta.DiscrTree.insertIfSpecific

deleted def Lean.Meta.DiscrTree.mapArrays

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic.lean

Deleted Mathlib/Tactic/Cache.lean

deleted def Mathlib.Tactic.Cache.get

deleted def Mathlib.Tactic.Cache.mk

deleted def Mathlib.Tactic.Cache

deleted def Mathlib.Tactic.DeclCache.get

deleted def Mathlib.Tactic.DeclCache.mk

deleted structure Mathlib.Tactic.DeclCache

deleted def Mathlib.Tactic.DiscrTreeCache.getMatch

deleted def Mathlib.Tactic.DiscrTreeCache.mk

deleted def Mathlib.Tactic.DiscrTreeCache

Modified Mathlib/Tactic/Common.lean

Modified Mathlib/Tactic/Find.lean

Deleted Mathlib/Tactic/LeftRight.lean

deleted def Mathlib.Tactic.LeftRight.leftRightMeta

Modified Mathlib/Tactic/LibrarySearch.lean

Modified Mathlib/Tactic/MkIffOfInductiveProp.lean

Modified Mathlib/Tactic/Propose.lean

Modified Mathlib/Tactic/Rewrites.lean

Modified lake-manifest.json

Deleted test/left_right.lean

deleted def two

deleted def zero

Modified test/propose.lean