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 · 2 comments · May be fixed by #261
Open

Declarations not hyperlinked #224

fpvandoorn opened this issue Oct 30, 2024 · 2 comments · May be fixed by #261

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.

@Komyyy
Copy link
Contributor

Komyyy commented Jan 10, 2025

@fpvandoorn
I built sign_apply in my branch and now it's hyperlinked. #261

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

Successfully merging a pull request may close this issue.

3 participants