Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Declarations not hyperlinked #224

Open
fpvandoorn opened this issue Oct 30, 2024 · 1 comment
Open

Declarations not hyperlinked #224

fpvandoorn opened this issue Oct 30, 2024 · 1 comment

Comments

@fpvandoorn
Copy link

In the type of some declarations, other declarations are not properly hyperlinked. For example
sign_apply does not link to SignType.sign.

Related to #104, which is about missing hyperlinks in markdown. Two examples in that issue aren't actually about markdown (Nat.toFinset_factors and WfDvdMonoid)

@kmill
Copy link
Contributor

kmill commented Nov 16, 2024

The sign_apply example is mostly a Lean pretty printing issue, and I think it should be fixed by leanprover/lean4#6085

The other ones involve fixing how docgen handles the terminfo. It needs to look to see if the getAppFn is a const, not that the expression itself is a const, like in the infoview. I did some experiments and it's a bit subtle to get right, since it can cause elements such as parentheses to become linkified.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants