Zulip Chat Archive

Stream: lean4

Topic: end a reopened namespace


view this post on Zulip Chris B (Feb 05 2021 at 20:15):

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

view this post on Zulip Mario Carneiro (Feb 05 2021 at 20:16):

You can do section open MyNamespace ... end

view this post on Zulip Chris B (Feb 05 2021 at 20:20):

That'll work. Much obliged.

view this post on Zulip Andrew Kent (Feb 05 2021 at 20:29):

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

view this post on Zulip Andrew Kent (Feb 05 2021 at 20:31):

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

view this post on Zulip Chris B (Feb 05 2021 at 20:41):

@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

Last updated: May 07 2021 at 12:15 UTC