This repository has been archived by the owner on Aug 24, 2024. It is now read-only.

LeanInk has trouble with infix operators #23

Open

lovettchris opened this issue Aug 25, 2022 · 0 comments

Labels

bug

Contributor

lovettchris commented Aug 25, 2022

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:

Suggested fix

Additional Notes

lovettchris added the bug label

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.