Commit 2023-05-22 03:13 8d402528

View on Github →

feat: add a global cache for the rewrites tactic (#4110)

Estimated changes

Modified Mathlib/Tactic/Cache.lean

added structure Mathlib.Tactic.CachedData

Modified Mathlib/Tactic/LibrarySearch.lean

deleted structure Mathlib.Tactic.LibrarySearch.CachedData

Modified Mathlib/Tactic/Rewrites.lean

added def Mathlib.Tactic.Rewrites.addLemma

added def Mathlib.Tactic.Rewrites.buildDiscrTree

added def Mathlib.Tactic.Rewrites.cachePath

added def Mathlib.Tactic.Rewrites.processLemma

added def Mathlib.Tactic.Rewrites.rewriteLemmas

modified def Mathlib.Tactic.Rewrites.rewrites

modified def Mathlib.Tactic.Rewrites.rewritesCore

Modified MathlibExtras.lean

Modified MathlibExtras/LibrarySearch.lean

Created MathlibExtras/Rewrites.lean

Modified test/rewrites.lean