Def Mathlib.Tactic.Linter.internalConstructor

Modification history

2026-09-03 17:31

Mathlib/Tactic/Linter/InternalConstructor.lean

feat: linter for internal constructors (#42883) …

Added Mathlib.Tactic.Linter.internalConstructor View on Github →