leanprover-community.github.io icon indicating copy to clipboard operation
leanprover-community.github.io copied to clipboard

yaml parsing has bug with same-title entries

Open hrmacbeth opened this issue 3 years ago • 1 comments

In the section "Hilbert spaces" of the undergrad.yaml file, there are two entries called "its completeness". It makes sense in context:

...
dual space: 'normed_space.dual.normed_space'
Riesz representation theorem: 'inner_product_space.to_dual'
inner product space $l^2$: 'lp.inner_product_space'
its completeness: 'lp.complete_space'
inner product space $L^2$: 'measure_theory.L2.inner_product_space'
its completeness: 'measure_theory.Lp.complete_space'
...

On the current display of the website, the first "its completeness" links to entry for the second "its completeness", and the second "its completeness" does not appear at all.

hrmacbeth avatar Jan 22 '22 05:01 hrmacbeth

I don't think it's worth making that code much more complicated for one example where we could simply change to "completeness of $l^2$" and "completeness of $L^2$"

PatrickMassot avatar Jan 22 '22 10:01 PatrickMassot