Commit 2022-11-03 22:33 4d4fafa9

View on Github →

chore: update std4 11-03 (#535) The main change is that guard_target and friends now use reducible defeq instead of syntactic eq by default.

Estimated changes

Modified Mathlib/Tactic/Cache.lean

added def Mathlib.Tactic.Cache.get

added def Mathlib.Tactic.Cache.mk

added def Mathlib.Tactic.Cache

added def Mathlib.Tactic.DeclCache.get

added def Mathlib.Tactic.DeclCache.mk

added def Mathlib.Tactic.DeclCache

deleted def Tactic.Cache.get

deleted def Tactic.Cache.mk

deleted def Tactic.Cache

deleted def Tactic.DeclCache.get

deleted def Tactic.DeclCache.mk

deleted def Tactic.DeclCache

Modified Mathlib/Tactic/Find.lean

added def Mathlib.Tactic.Find.findType

deleted def Tactic.Find.findType

Modified Mathlib/Tactic/LibrarySearch.lean

added def Mathlib.Tactic.LibrarySearch.librarySearch

added def Mathlib.Tactic.LibrarySearch.lines

added def Mathlib.Tactic.LibrarySearch.solveByElim

deleted def Tactic.LibrarySearch.librarySearch

deleted def Tactic.LibrarySearch.lines

deleted def Tactic.LibrarySearch.solveByElim

Modified lean_packages/manifest.json

Modified scripts/nolints.json

Modified test/Contrapose.lean

Modified test/PermuteGoals.lean

Modified test/Set.lean

Modified test/Simps.lean

Modified test/SwapVar.lean

Modified test/Use.lean

Modified test/Zify.lean

Modified test/basicTactics.lean

Modified test/cases.lean

Modified test/convert.lean

Modified test/fin_cases.lean

Modified test/norm_cast.lean

Modified test/push_neg.lean

Modified test/rcases.lean

Modified test/simp_intro.lean