section interposing with namespace

Stream: general

[Kenny Lau]

Is it possible to have the following?

section foo
namespace bar
end foo
end bar

[Johan Commelin]

I think it is not obvious how exactly that should behave

[Kenny Lau]

section foo
variable (X : Type)
constant A : Type
-- scope: X, A

namespace bar
variable (Y : Type)
constant B : Type
-- scope: X, Y, A, B

end foo
variable (Z : Type)
constant C : Type
-- scope: Y, Z, A, B, C

end bar
-- scope: A, bar.B, bar.C

[Kenny Lau]

variable-wise, there is no difference between section and namespace

[Kenny Lau]

declaration-wise, everything inside a namespace gets a prefix

[Kenny Lau]

@Johan Commelin is this natural?

[Johan Commelin]

But what happens if I add variable [group X] between namespace bar and end foo?

[Johan Commelin]

I guess that should also be gone after the end foo, but it will probably make the bookkeeping more complicated.

[Kenny Lau]

that's exactly why I proposed it. I want to change from ring to field without ending the namespace

[Kenny Lau]

section ring

variables (R : Type) [ring R]

def foo := R

namespace foo

lemma bar : foo = foo := rfl

end ring

section field

variables (F : Type) [field F]

lemma bar' : foo = foo := rfl

end field

end foo

[Kenny Lau]

hmm, looks like I misunderstood you

[Kenny Lau]

but this is my intended use-case anyway

[Mario Carneiro]

I think this would be a bad idea with the current design, because section ... end and namespace ... end act like matched pairs

[Mario Carneiro]

If you want to do tricks like that it should be with another, non-scoping namespace mechanism like set_namespace foo, set_namespace _root_ or the like