Def Batteries.Tactic.Lint.deprecatedNoSince

Modification history

2024-09-25 00:50

Mathlib/Tactic/Linter/Lint.lean

chore: bump dependencies and adapt to updated namespaces (#17117)

Added Batteries.Tactic.Lint.deprecatedNoSince View on Github →