Zulip Chat Archive

Stream: new members

Topic: 'open' vs 'namespace'

kaminsod (Jun 08 2021 at 02:03):

What is the fundamental difference between 'open' and 'namespace' ? They seem somewhat interchangeable?

Bryan Gin-ge Chen (Jun 08 2021 at 02:05):

namespace foo adds foo. to the beginning of the names of all new declarations until end foo.

open foo simply lets you refer to theorems like foo.bar as bar.

See this section of TPiL for more details.

Johan Commelin (Jun 08 2021 at 02:22):

In addition, namespace foo also acts as open foo.

kaminsod (Jun 08 2021 at 02:25):

Makes sense, thanks!

Last updated: Dec 20 2023 at 11:08 UTC