Defines with_weak_namespace command.

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

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

Adds the name to the namespace, _root_-aware.

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

Equations

• Lean.Elab.Command.resolveNamespace ns `_root_ = Lean.Name.anonymous
• Lean.Elab.Command.resolveNamespace ns (n.str s) = (Lean.Elab.Command.resolveNamespace ns n).mkStr s
• Lean.Elab.Command.resolveNamespace ns (n.num i) = (Lean.Elab.Command.resolveNamespace ns n).mkNum i
• Lean.Elab.Command.resolveNamespace ns Lean.Name.anonymous = ns

def Lean.Elab.Command.withWeakNamespace {α : Type} (ns : Lean.Name) (m : Lean.Elab.Command.CommandElabM α) : Lean.Elab.Command.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__ : Lean.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.