doc-gen4 linking specification

Stream: lean4

[Gabriel Ebner]

@Henrik Böving @Xubai Wang Is there a specification for the markdown links to declarations written down somewhere? I vaguely recall that it's something like [Link text](##qualified.declaration.name).

[Henrik Böving]

There are two ways, all things in backtick quotes are attempted to link automatically by looking it up in the global and local namespace https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/DocString.lean#L62-L68 and there is the other things: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/DocString.lean#L94-L101 though I dont think we've really tested that in all of its facets at least i certainly did not.

[Henrik Böving]

I've been planning to extend on the markdown capabilities etc. when I'm done with this semesters exams so we can render the leanink parts nicer as well

[Gabriel Ebner]

Once you're free again we should write down the Lean markdown dialect somewhere. @Chris Lovett wants to add go-to-declaration to the links in the markdown docstrings and it would be good to use the same standard everywhere.