Documentation

Mathlib.Util.WithWeakNamespace

Defines with_weak_namespace command. #

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

Adds the name to the namespace, _root_-aware.

resolveNamespace `A `B.b == `A.B.b
resolveNamespace `A `_root_.B.c == `B.c
Equations
    Instances For

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

      Equations
        Instances For

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

          Equations
            Instances For