Autolinking in docs

Stream: general

[Eric Wieser]

I notice that the link to leval in docs#finsupp.leval' does not work. Is that because it ought to be spelt finsupp.leval, or can links only point to definitions that come before the current definition?

[Gabriel Ebner]

They need to be fully-qualified names.

[Yury G. Kudryashov]

BTW, how should we link to other lean files in the docs?

[Gabriel Ebner]

How about relative links in the markdown files?

/--
... [finitely-supported functions](../../data/finsupp/basic.lean) ...
-/

(no file links are supported yet)

[Yury G. Kudryashov]

And doc-gen will have to replace .lean with .html?

[Gabriel Ebner]

Yes.