Def Mathlib.Linter.DocPrime.docPrimeLinter

Modification history

2024-09-25 13:34
Mathlib/Tactic/Linter/DocPrime.lean
feat: the docPrime linter (#16694) …
Added Mathlib.Linter.DocPrime.docPrimeLinterView on Github →