The Category Linter

The categoryLinter is a linter to aid with formatting contributions to the Formal Conjectures repository by ensuring that results in a file have the appropriate tags in order to distinguish between open/already solved problems and background results/sanity checks.

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

Checks if a command has the category attribute.

Equations

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

def CategoryLinter.categoryLinter : Lean.Linter

The problem category linter checks that every theorem/lemma/example has been given a problem category attribute.

Equations

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