## Stream: general

### Topic: namespaces inside sections

#### Patrick Massot (Nov 20 2020 at 09:01):

@Sebastian Ullrich I see that namespaces are not allowed inside sections in Lean 4. This is a very frustrating restriction and Gabriel got rid of it in Lean 3. Is there any reason to keep it in Lean 4?

#### Johan Commelin (Nov 20 2020 at 09:26):

@Patrick Massot I think you wanted to link to https://github.com/leanprover/lean4/blob/master/doc/namespaces.md
In the docs on sections, I didn't see any mention of this restriction.

#### Gabriel Ebner (Nov 20 2020 at 09:27):

The commit message was very pessimistic. AFAICR we didn't find a single horribly broken corner case.

#### Kevin Buzzard (Nov 20 2020 at 09:42):

Funnily enough I might have found one at Xena yesterday, regarding include. Let me see if I can reproduce.

#### Kevin Buzzard (Nov 20 2020 at 09:44):

This file https://github.com/ImperialCollegeLondon/M40002/blob/master/src/problem_sheet_two.lean breaks when you put the entire contents within a namespace. I'll minimise.

#### Gabriel Ebner (Nov 20 2020 at 09:45):

My first instinct was "ctrl+f parameter", and indeed it found something. I woudln't be surprised if that was the issue.

#### Kevin Buzzard (Nov 20 2020 at 09:49):

Yes it's parameters. Are they problematic within a namespace? I can't put these theorems in a namespace:

import data.real.basic

--namespace foo

section Q4

noncomputable theory

section two

parameters {a : ℝ} (ha : 0 < a) {n : ℕ} (hn : 0 < n)

include ha hn

def S := {s : ℝ | 0 ≤ s ∧ s ^ n < a}

def x := Sup S

theorem is_lub_x : is_lub S x :=
begin
sorry,
end

lemma x_nonneg : 0 ≤ x :=
begin
rcases is_lub_x with ⟨h, -⟩,
sorry
end

end two

end Q4

--end foo


#### Kevin Buzzard (Nov 20 2020 at 09:54):

Mathlib-free. Is this a known issue? I was surprised. Uncomment the namespace and end lines and I get an error.

--namespace foo

section two

parameters {a : ℕ} (ha : 0 < a)

include ha

def x := 37

theorem is_lub_x : x = 37 :=
begin
refl
end

lemma x_nonneg : 0 ≤ x :=
begin
have h : x = 37 := is_lub_x,
sorry
end

end two

--end foo


#### Sebastian Ullrich (Nov 21 2020 at 09:23):

Johan Commelin said:

Patrick Massot I think you wanted to link to https://github.com/leanprover/lean4/blob/master/doc/namespaces.md
In the docs on sections, I didn't see any mention of this restriction.

The sentence is gone; the restriction didn't actually exist :)

Last updated: May 12 2021 at 23:13 UTC