Topic: autolinks in docs
Yury G. Kudryashov (Mar 13 2020 at 03:28):
Would it be hard to (a) automatically create link targets for all definitions/lemmas (e.g., using their full names) to allow something like
[monoid homomorphism](monoid_hom); (b) automatically turn
monoid_hom in a docstring into a link to the definition of
Rob Lewis (Mar 13 2020 at 09:10):
Any full identifier that appears in backticks should (in principle) be linkified already in the HTML docs. See e.g.
euclidean_space at https://leanprover-community.github.io/mathlib_docs/geometry/manifold/real_instances.html . A few catches:
- There's clearly a bug here, since some occurrences in that module doc don't get linked. Maybe it's missing the first token of each block? I'll investigate.
- You need to use full identifiers,
nat.succinstead of just
- I'm not sure it's firing for declaration doc strings, but if not, this is an easy fix.
Last updated: Aug 03 2023 at 10:10 UTC