end a reopened namespace

Stream: lean4

[Chris B]

Is there a way to end a reopened namespace to hide the abbreviated names? The current set of docs ends after mentioning the ability to reopen the namespace.

namespace MyNamespace
  def Num : Nat := 0
end MyNamespace

open MyNamespace
-- do stuff with shortened names
end MyNamespace
--  ^^ invalid 'end', insufficient scopes

[Mario Carneiro]

You can do section open MyNamespace ... end

[Chris B]

That'll work. Much obliged.

[Andrew Kent]

If it's just for a single definition or similar, you can use open ... in ... and it will just apply to the subsequent term I believe

[Andrew Kent]

from Lean's src/Lean/Compiler/Util.lean:

open atMostOnce (visit) in
/-- Return true iff the free variable with id `x` occurs at most once in `e` -/
@[export lean_at_most_once]
def atMostOnce (e : Expr) (x : Name) : Bool :=
  let {result := result, ..} := visit x e {found := false, result := true}
  result

[Chris B]

@Andrew Kent

Good eye, that seems to work even for commands:

namespace MyNamespace
  def Num : Nat := 0
end MyNamespace

-- works
open MyNamespace in #print Num

-- doesn't work; closed again
#print Num