## Description This works fine in my applicative.lean source file when loaded in VS code, when when I process the book I get these weird tooltips:  ## Expected behaviour Same tooltips I get in VS code, or at least not this weird error message. ## Reproducing the issue Build the reference manual with this PR: https://github.com/leanprover/lean4/pull/1505 ## Environment information - Operating System: - Lean version: - LeanInk version: - Alectryon version: ## Suggested fix <!--- You have an idea on how to fix the bug? List it here so we can discuss it. --> ## Additional Notes <!-- Any other notes which are inappropriate in the other categories -->
Description
This works fine in my applicative.lean source file when loaded in VS code, when when I process the book I get these weird tooltips:
Expected behaviour
Same tooltips I get in VS code, or at least not this weird error message.
Reproducing the issue
Build the reference manual with this PR: leanprover/lean4#1505
Environment information
Suggested fix
Additional Notes