How to end a scope?

Stream: new members

[Darij Grinberg]

I can open a scope in Lean using open. How do I close it?

[Kenny Lau]

enclose it in a section/namespace

[Arthur Paulino]

I think it would be nice to be able to close it within the same section or namespace.

@Darij Grinberg you can also do

open Foo in
def bar ...

Which opens the Foo scope limited to bar

[Darij Grinberg]

ah!

[Kenny Lau]

i think it's possible, i'm trying to do it rn

[Kenny Lau]

import Lean

def Lean.OpenDecl.match (n : Name) : OpenDecl → Bool
  | .simple a _b => a == n
  | .explicit a _b => a == n

namespace Lean.Elab.Command

def Scope.close (n : Name) (sc : Scope) : Scope :=
  { sc with openDecls := sc.openDecls.filter (!OpenDecl.match n ·) }

elab "close " ns:ident : command =>
  modifyScope <| Scope.close ns.getId

end Lean.Elab.Command

section Test

#check Nat.add_mod
#check add_mod -- error

open Nat

#check Nat.add_mod
#check add_mod

close Nat

#check Nat.add_mod
#check add_mod -- error

end Test

[Kenny Lau]

the #xy continues...

[Darij Grinberg]

wow, I didn't know Lean code could modify itself this easily

[Darij Grinberg]

but yeah, i can wrap my scopes in sections, no problem with that

[Kenny Lau]

image.png

so that means i can also delete variables... i've wanted that feature for a while

[Junyan Xu]

so that means i can also delete variables... i've wanted that feature for a while

Is omit not good enough?

[Kenny Lau]

@Junyan Xu see #mathlib4 > RFC: delete variables