Add delaborator checking canonicity of instances
#33.238 geöffnet am 23.12.2025
Repository-Metriken
- Stars
- (3.869 Sterne)
- PR-Merge-Metriken
- (Keine gemergten PRs in 30 T)
Beschreibung
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.