The Category Docstring Linter

The CategoryDocstringLinter ensures that declarations tagged as @[category research open], @[category research solved], or @[category textbook] have a docstring.

opaque linter.style.category_docstring : Lean.Option Bool

def CategoryDocstringLinter.toCategorySyntax (stx : Lean.TSyntax `Lean.Parser.Command.declModifiers) : Lean.Elab.Command.CommandElabM (Array (Lean.TSyntax `Lean.Parser.Term.attrInstance))

Extract the category attributes from a declaration's modifiers.

Equations

• One or more equations did not get rendered due to their size.

def CategoryDocstringLinter.toCategories (stx : Lean.TSyntax `Lean.Parser.Command.declModifiers) : Lean.Elab.Command.CommandElabM (Array ProblemAttributes.Category)

Extract the categories from a declaration's modifiers.

Equations

• One or more equations did not get rendered due to their size.

def CategoryDocstringLinter.categoryNeedsDocstring : ProblemAttributes.Category → Bool

Whether the given category requires a docstring.

Equations

• CategoryDocstringLinter.categoryNeedsDocstring (ProblemAttributes.Category.research ProblemAttributes.ProblemStatus.open) = true
• CategoryDocstringLinter.categoryNeedsDocstring (ProblemAttributes.Category.research ProblemAttributes.ProblemStatus.solved) = true
• CategoryDocstringLinter.categoryNeedsDocstring ProblemAttributes.Category.textbook = true
• CategoryDocstringLinter.categoryNeedsDocstring x✝ = false

def CategoryDocstringLinter.hasDocstring (stx : Lean.TSyntax `Lean.Parser.Command.declModifiers) : Bool

Whether the declaration modifiers contain a docstring.

Equations

• CategoryDocstringLinter.hasDocstring stx = !stx.raw[0]![0]![1]!.getAtomVal.isEmpty

def CategoryDocstringLinter.categoryDocstringLinter : Lean.Linter

The linter checking for docstrings on research statements.

Equations

• One or more equations did not get rendered due to their size.