Accessing shadowed names?

Stream: new members

[Martin Suda]

Is there way to access Lean's true Nat from the my_nat namespace below, after the local Nat has been defined?

namespace my_nat

inductive Nat : Type
  | zero : Nat
  | succ : Nat -> Nat

#print Nat

end my_nat

In C++, e.g., this could be something like ::Nat or something like that.

[Damiano Testa]

You can prepend _root_., as in _root_.Nat.

[Martin Suda]

Thank you!