accessing function outside of namespace

Stream: new members

[Nir Paz]

When working in a namespace that defines a function with a name x that's already used outside of it, how can I access the outer x? I know I can use && in my case but is there a more general way to step out of a namespace for a term?

inductive Form where
  | and : Form → Form → Form

example (a b : Bool) : Bool := and a b -- works

namespace Form

example (a b : Bool) : Bool := and a b -- fails

The Boolean and isn't defined in a namespace so there isn't a "full name" I can use.

[Nir Paz]

Figured out I can use _root_.