The "implicit namespace" linter

Original code written by Damiano Testa.

The "implicitNamespace" linter emits a warning when a declaration uses the "implicit namespace" feature, see explanation: https://github.com/leanprover/lean4/issues/6855

opaque Mathlib.Linter.linter.implicitNamespace : Lean.Option Bool

The "implicitNamespace" linter emits a warning when a declaration uses the "implicit namespace" feature.

def Mathlib.Linter.ImplicitNamespace.implicitNamespaceLinter : Lean.Linter

The "implicitNamespace" linter emits a warning when a declaration uses the "implicit namespace" feature.

Equations

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