Error in documentation links

Stream: general

[Julia Scheaffer]

I was looking at the docs on List.Vector and many of the definitions seems to have links to Vector instead of List.Vector (example: List.Vector.«term_::ᵥ_» ) is this a bug in the docs?

[Bryan Gin-ge Chen]

The docstrings might need to be changed to have List.Vector instead of Vector for the links to work properly.

[Kenny Lau]

what is the algorithm of determining the link?

[Ruben Van de Velde]

I think the links used to work before we renamed Vector to List.Vector

[Henrik Böving]

It's a heuristic at the moment: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/DocString.lean#L70-L96 note that as David is working on integration verso with docstrings in the not so distant future we are going to have a much more predictable model that you can actually inspect directy in your editor as well for this.