source for `open `

Stream: mathlib4

[Antoine Chambert-Loir]

The instructions open BigOperators, open Classical, open CategoryTheory open a local context of notation and lemmas.

• How to know what is actually available?

• How to know which local contexts exist and what they do?

[Kyle Miller]

open ns now does two things: it makes it so that you can refer to ns.foo as foo, and it causes all of the scoped attributes to become locally activated. Attributes are how notations and instances are added to the system in general. There's also open scoped ns to only locally add the scoped attributes.

It would be great if docgen could generate two extra sorts of documentation:

1. An index of all lemmas and definitions by namespace (in addition to lemmas and definitions by module). That solves the question of what you can refer to unqualified when you do open ns.

2. An index of things that are scoped by namespace.

In the meantime, you can search for "scoped" in the source and exclude "open scoped"...