My proposal to address this would be to record the namespaces that were open when a definition was done in an environment extension. This extension could then be introspected by doc-gen in order to pretty print declarations that used scoped notation correctly.
Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.
Kha
commented
1 week ago
Proposal
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/docgen.20scoped.20notations/near/481956588 brought up the issue of scoped notation within doc-gen. As the post shows we currently have no way to know precisely what notations where available when a theorem or definition was declared.
My proposal to address this would be to record the namespaces that were open when a definition was done in an environment extension. This extension could then be introspected by doc-gen in order to pretty print declarations that used scoped notation correctly.
Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.