Zulip Chat Archive

Stream: general

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 monoid_hom?

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.succ instead of just succ.
  • 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