opaque Lean.Linter.Extra.linter.extra.dupNamespace : Lean.Option Bool

The dupNamespace linter is set off by default. Lean emits a warning on any declaration that contains the same namespace at least twice consecutively.

For instance, Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not.

Note. This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose declId is present in the source declaration).

def Lean.Linter.Extra.DupNamespaceLinter.getNamesFrom {m : Type → Type} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos.Raw) : m (Array Syntax)

If pos is a String.Pos, then getNamesFrom pos returns the array of identifiers for the names of the declarations whose syntax begins in position at least pos.

Equations

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

def Lean.Linter.Extra.DupNamespaceLinter.getAliasSyntax {m : Type → Type} [Monad m] [MonadResolveName m] (stx : Syntax) : m (Array Syntax)

If stx is a syntax node for an export statement, then getAliasSyntax stx returns the array of identifiers with the "exported" names.

Equations

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

def Lean.Linter.Extra.DupNamespaceLinter.dupNamespace : Linter

The dupNamespace linter is set off by default. Lean emits a warning on any declaration that contains the same namespace at least twice consecutively.

For instance, Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not.

Note. This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose declId is present in the source declaration).

Equations

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