autolinks in docs

Stream: general

[Yury G. Kudryashov]

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]

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.