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 more than once.

By default, only consecutive duplication is reported: Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not. Setting linter.extra.dupNamespace.consecutiveOnly to false also reports non-consecutive duplication, so that Nat.One.Nat triggers a warning as well.

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

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 more than once.

By default, only consecutive duplication is reported: Nat.Nat.foo and One.two.two trigger a warning, while Nat.One.Nat does not. Setting linter.extra.dupNamespace.consecutiveOnly to false also reports non-consecutive duplication, so that Nat.One.Nat triggers a warning as well.

Equations

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