search

leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

Generate hyperlinks for `library note [XYZ]` to the corresponding `library_note` doc-string. #135

Open semorrison opened 1 year ago

semorrison commented 1 year ago

See https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Basis.html#Basis.constr for an example.

There we would like in "See library note [bundled maps over different rings]." for "bundled maps over different rings" to hyperlink to the doc-comment in Mathlib.GroupTheory.GroupAction.Defs, and moreover for the library_note in that file to actually be rendered on the documentation page! (It should come just above VAddCommClass.)

semorrison commented 1 year ago

https://github.com/leanprover/vscode-lean4/issues/286 is the corresponding open issue for making library notes clickable in VSCode.