namespace inside section

Stream: general

[Reid Barton]

Is there a compelling reason to not be able to put a namespace inside a section?

[Reid Barton]

Maybe changing in this in Lean 3 would be too much.

[Kenny Lau]

namespace test1
section test2
namespace test3
section test4
end test4
end test3
end test2
end test1

[Kenny Lau]

does anyone remember the time when we weren't allowed to put a namespace inside a section? what happened?

[Kevin Buzzard]

Ooh! I was going to bring this up the other day! You've spared my blushes :-)

[Bryan Gin-ge Chen]

lean#317 happened

[Bryan Gin-ge Chen]

(Thanks @Gabriel Ebner !)

[Scott Morrison]

I wish I could remember all the times I've previously had to work around this, so I could go back and fix them!

[Scott Morrison]

Actually maybe just looking for

end X

begin X

(done to clear variables) would find many of them.