You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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)
The text was updated successfully, but these errors were encountered:
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.
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)
The text was updated successfully, but these errors were encountered: