Zulip Chat Archive
Stream: new members
Topic: namespace inside section
Kenny Lau (Jun 23 2019 at 14:49):
Why can't a namespace be declared inside a section?
Mario Carneiro (Jun 23 2019 at 14:49):
because lean says so
Johan Commelin (Jun 23 2019 at 17:57):
I've also wished for the absence of this "feature" . @Sebastian Ullrich will this change in :four: ?
Sebastian Ullrich (Jun 23 2019 at 18:17):
@Johan Commelin Absolutely
Last updated: May 02 2025 at 03:31 UTC