Zulip Chat Archive

Stream: general

Topic: namespaces inside sections


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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