Commit 2022-02-07 13:35 147444b2

View on Github →

chore: bump to nightly-2022-02-07 (#186)

Estimated changes

Modified Mathlib/Tactic/Lint/Simp.lean

deleted structure Mathlib.Tactic.Lint.SimpLemmaInfo

added structure Mathlib.Tactic.Lint.SimpTheoremInfo

deleted def Mathlib.Tactic.Lint.checkAllSimpLemmaInfos

added def Mathlib.Tactic.Lint.checkAllSimpTheoremInfos

deleted def Mathlib.Tactic.Lint.heuristicallyExtractSimpLemmas

deleted def Mathlib.Tactic.Lint.heuristicallyExtractSimpLemmasCore

added def Mathlib.Tactic.Lint.heuristicallyExtractSimpTheorems

added def Mathlib.Tactic.Lint.heuristicallyExtractSimpTheoremsCore

deleted def Mathlib.Tactic.Lint.isSimpLemma

added def Mathlib.Tactic.Lint.isSimpTheorem

deleted def Mathlib.Tactic.Lint.withSimpLemmaInfos

added def Mathlib.Tactic.Lint.withSimpTheoremInfos

Modified Mathlib/Tactic/NormCast.lean

Modified lean-toolchain