Add delaborator checking canonicity of instances
#33.238 aberto em 23 de dez. de 2025
Métricas do repositório
- Stars
- (3.869 estrelas)
- Métricas de merge de PR
- (Nenhuma PRs mesclada em 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.