LeanInk has trouble with infix operators - Githubissues

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

Apache License 2.0

60 stars 16 forks source link

LeanInk has trouble with infix operators #23

Open lovettchris opened 2 years ago

lovettchris commented 2 years ago

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

Additional Notes