The AMS Linter

The AMSLinter is a linter to aid with formatting contributions to the Formal Conjectures repository by ensuring that results in a file have the appropriate subject tags.

def AMSLinter.toAMS (stx : Lean.TSyntax `Lean.Parser.Command.declModifiers) : Lean.Elab.Command.CommandElabM (Array (Lean.TSyntaxArray `num))

Checks if a command has the AMS attribute.

Equations

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

def AMSLinter.mkAMSSyntax (nums : Lean.TSyntaxArray `num) : Lean.Elab.Command.CommandElabM (Lean.TSyntax `Lean.Parser.Term.attrInstance)

Equations

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

def AMSLinter.AMSLinter : Lean.Linter

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

Equations

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