Add delaborator checking canonicity of instances
#33.238 aperta il 23 dic 2025
Metriche repository
- Star
- (3869 stelle)
- Metriche merge PR
- (Nessuna PR mergiata in 30 g)
Descrizione
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.