Limiting the scope of a definition

Stream: lean4

[The-Anh Vu-Le]

Hi, is it possible to define something that only exists inside a section? For example, I would like to write something like this.

import Mathlib.Data.Set.Basic

section

def S : Set ℕ := {1, 2, 3}

example : 1 ∈ S := by sorry

end

section

def S : Set ℕ := {2, 3}

example : 1 ∉ S := by sorry

end

[Damiano Testa]

Is private what you are looking for?

[Damiano Testa]

Sorry, private is not "local" to a section.

[The-Anh Vu-Le]

private doesn't have that effect. The below gives private declaration 'S' has already been declared. Any other combination does not work either.

import Mathlib.Data.Set.Basic

section

private def S : Set ℕ := {1, 2, 3}

example : 1 ∈ S := by sorry

end

section

private def S : Set ℕ := {2, 3}

example : 1 ∉ S := by sorry

end

[Damiano Testa]

Couldn't you use namespace instead of section?

[The-Anh Vu-Le]

I just want to avoid naming many things, so I was hoping for a way to do scoping with section.

[Damiano Testa]

I think that section is mostly a way to limit the scope of variable, open, set_options.

[Damiano Testa]

I can't think right now of something that limits the scope of declarations and I suspect that private might be the only such mechanism, but it works with imports, not inside the same module.

[Kyle Miller]

Yeah, private is the only mechanism, and it's across module boundaries.

I use namespace for this purpose (for example in test files with multiple tests that each involve definitions, each test gets its own namespace)

[Kyle Miller]

import Mathlib.Data.Set.Basic

namespace Sec1

def S : Set ℕ := {1, 2, 3}

example : 1 ∈ S := by sorry

end Sec1

namespace Sec2

def S : Set ℕ := {2, 3}

example : 1 ∉ S := by sorry

end Sec2

[Kyle Miller]

I'm not sure it's a good idea, but it should be relatively straightforward to make a namespace*/end* pair of commands that enter a namespace with a fresh name and then leave it. I'm not sure exactly how to make end* check that it's leaving a namespace*-created namespace, unless namespace* uses some fixed prefix it matches on.

[Niels Voss]

What about calling it namespace _?

[Jz Pan]

private namespace?