Zulip Chat Archive

Stream: general

Topic: section interposing with namespace


Kenny Lau (Oct 20 2020 at 09:03):

Is it possible to have the following?

section foo
namespace bar
end foo
end bar

Johan Commelin (Oct 20 2020 at 09:04):

I think it is not obvious how exactly that should behave

Kenny Lau (Oct 20 2020 at 09:06):

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 (Oct 20 2020 at 09:07):

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

Kenny Lau (Oct 20 2020 at 09:07):

declaration-wise, everything inside a namespace gets a prefix

Kenny Lau (Oct 20 2020 at 09:09):

@Johan Commelin is this natural?

Johan Commelin (Oct 20 2020 at 09:09):

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

Johan Commelin (Oct 20 2020 at 09:10):

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

Kenny Lau (Oct 20 2020 at 09:11):

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

Kenny Lau (Oct 20 2020 at 09:13):

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 (Oct 20 2020 at 09:13):

hmm, looks like I misunderstood you

Kenny Lau (Oct 20 2020 at 09:13):

but this is my intended use-case anyway

Mario Carneiro (Oct 20 2020 at 15:27):

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

Mario Carneiro (Oct 20 2020 at 15:28):

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


Last updated: Dec 20 2023 at 11:08 UTC