LeanInk has trouble with infix operators
Opened this issue · 0 comments
lovettchris commented
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
- Operating System:
- Lean version:
- LeanInk version:
- Alectryon version: