What question should the reference manual answer?
There are two separate but related issues with https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#module-scopes currently:
@[no_expose] isn't documented
@[expose] is only documented in relation to def, leaving implicit what @[expose]/@[no_expose] do to an abbrev. instance, structure, class, in particular what the default exposition is for each of these.
Additional context
Zulip
What question should the reference manual answer?
There are two separate but related issues with https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#module-scopes currently:
@[no_expose]isn't documented@[expose]is only documented in relation todef, leaving implicit what@[expose]/@[no_expose]do to anabbrev.instance,structure,class, in particular what the default exposition is for each of these.Additional context
Zulip