Defines with_weak_namespace command.

Changes the current namespace without causing scoped things to go out of scope.

partial def Lean.Elab.Command.resolveNamespace (ns : Name) : Name → Name

Adds the name to the namespace, _root_-aware.

resolveNamespace `A `B.b == `A.B.b
resolveNamespace `A `_root_.B.c == `B.c

def Lean.Elab.Command.withWeakNamespace {α : Type} (ns : Name) (m : CommandElabM α) : CommandElabM α

Changes the current namespace without causing scoped things to go out of scope

Equations

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

def Lean.Elab.Command.commandWith_weak_namespace__ : ParserDescr

Changes the current namespace without causing scoped things to go out of scope

Equations

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