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

Issues: leanprover/LeanInk

12 Open 15 Closed
12 Open 15 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Error when analyzing a simple file with LeankInk: failed to read file ..., invalid header bug Something isn't working
#59 opened Aug 13, 2024 by mariovagomarzal
Using Mathlib as an import causes leanInk to error bug Something isn't working
#56 opened Dec 28, 2023 by femtomc
We need to get back the "Copy to clipboard" button on Lean code snippets
#35 opened Oct 8, 2022 by lovettchris
Red squiggles enhancement New feature or request
#34 opened Sep 8, 2022 by lovettchris
We need to get back the "Try It" button when manual is read inside VS code documentation view enhancement New feature or request
#32 opened Sep 2, 2022 by lovettchris
Provide the mdbook # namespace hidden trick
#30 opened Aug 31, 2022 by lovettchris
1
Provide a way to tell leanink to generate comments on #eval, #check commands
#29 opened Aug 30, 2022 by lovettchris
2
Hiding certain Lean imports at the beginging of a chapter
#25 opened Aug 26, 2022 by lovettchris
LeanInk silently eats lean compile errors bug Something isn't working
#24 opened Aug 26, 2022 by lovettchris
1
LeanInk has trouble with infix operators bug Something isn't working
#23 opened Aug 25, 2022 by lovettchris
Colorization difference bug Something isn't working
#22 opened Aug 25, 2022 by lovettchris
LeanInk can't install itself for brew-installed elan bug Something isn't working
#21 opened Aug 1, 2022 by utensil
10
ProTip! Mix and match filters to narrow down what you’re looking for.