def
Lean.Linter.checkAmbiguousOpen
{m : Type → Type}
[Monad m]
[MonadEnv m]
[MonadOptions m]
[MonadLog m]
[AddMessageContext m]
[MonadResolveName m]
(nsStx : Ident)
(resolved : List Name)
:
m Unit
Warns if the namespace identifier nsStx of an open declaration can also be interpreted as an
existing namespace that the open declaration silently does not open. resolved must be the
interpretations the open declaration actually uses, as returned by resolveNamespace.
Shadowed interpretations whose declarations are accessible anyway — because the namespace is
already opened without exceptions or encloses the current scope — are not reported.
Equations
- One or more equations did not get rendered due to their size.