The Namespace Linter

The namespaceLinter is a linter to aid with formatting contributions to the Formal Conjectures repository by ensuring that all declarations are placed within a namespace.

opaque NamespaceLinter.linter.style.namespace : Lean.Option Bool

The namespace linter is set on by default. It emits a warning on any declaration that is not inside a namespace (i.e., declarations at the root level).

For instance, theorem foo would trigger a warning, while Nat.foo would not.

This helps maintain organization and avoid polluting the global namespace.

def NamespaceLinter.namespaceLinter : Lean.Linter

The namespace linter checks that every declaration is inside a namespace.

Equations

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