Add delaborator checking canonicity of instances
#33,238 opened on Dec 23, 2025
Repository metrics
- Stars
- (3,405 stars)
- PR merge metrics
- (No merged PRs in 30d)
Description
Following a Zulip discussion https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Topological.20.28scoped.29.20notation.20in.20doc-gen/near/565193294 I'm suggesting that we introduce some fix to (topological) scoped notation not showing up in the doc-gen.
More concretely, observe that on this file one finds the definition of open/closed/etc... with respect to non-standard topologies, so that one can write IsOpen[T] (U : Set X), for instance, to mean that a set U is open wrt to the topology T rather than wrt any other topology that might be synthesized on X. This I find very convenient, but it does not show up in the doc-gen so that, for example, while reading docs#LinearMap.mem_span_iff_continuous_of_finite online one has no clue of the topology on E with respect to which φ would be continuous — whereas in the source this is very clear.