This repository was archived by the owner on Aug 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 18
Issues
is:issue state:open
is:issue state:open
Search results
Error when analyzing a simple file with
LeankInk:failed to read file ..., invalid headerbugSomething isn't workingSomething isn't workingStatus: Open.#59 In leanprover/LeanInk;Using
Mathlibas an import causesleanInkto errorbugSomething isn't workingSomething isn't workingStatus: Open.#56 In leanprover/LeanInk;- Status: Open.#35 In leanprover/LeanInk;
Red squiggles
enhancementNew feature or requestNew feature or requestStatus: Open.#34 In leanprover/LeanInk;We need to get back the "Try It" button when manual is read inside VS code documentation view
enhancementNew feature or requestNew feature or requestStatus: Open.#32 In leanprover/LeanInk;- Status: Open.#30 In leanprover/LeanInk;
- Status: Open.#29 In leanprover/LeanInk;
- Status: Open.#25 In leanprover/LeanInk;
LeanInk silently eats lean compile errors
bugSomething isn't workingSomething isn't workingStatus: Open.#24 In leanprover/LeanInk;LeanInk has trouble with infix operators
bugSomething isn't workingSomething isn't workingStatus: Open.#23 In leanprover/LeanInk;Colorization difference
bugSomething isn't workingSomething isn't workingStatus: Open.#22 In leanprover/LeanInk;LeanInk can't install itself for brew-installed elan
bugSomething isn't workingSomething isn't workingStatus: Open.#21 In leanprover/LeanInk;