leanprover/LeanInk
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
LeanApache-2.0
Issues
- 0
Error when analyzing a simple file with `LeankInk`: `failed to read file ..., invalid header`
#59 opened by mariovagomarzal - 0
- 0
- 0
Red squiggles
#34 opened by lovettchris - 10
- 0
We need to get back the "Try It" button when manual is read inside VS code documentation view
#32 opened by lovettchris - 1
Provide the mdbook `# namespace hidden` trick
#30 opened by lovettchris - 2
Provide a way to tell leanink to generate comments on #eval, #check commands
#29 opened by lovettchris - 1
LeanInk silently eats lean compile errors
#24 opened by lovettchris - 4
Error with custom notation
#27 opened by lecopivo - 0
- 0
LeanInk has trouble with infix operators
#23 opened by lovettchris - 0
Colorization difference
#22 opened by lovettchris - 3
- 2
No types or goals inside matches
#15 opened by Kha - 0
Alectryon Type Information on hover
#11 opened by insightmind - 0
Lean 4 syntax highlighting in Alectryon
#10 opened by insightmind - 0
Wrong Typename exported
#13 opened by insightmind - 0
- 0
- 0
Implement Lean 4 driver in Alectryon
#7 opened by insightmind - 4
Load LeanSearchPaths
#9 opened by insightmind - 11
Evaluate Alectryon extensibility
#1 opened by insightmind - 3
Implement first working prototype
#3 opened by insightmind - 1
Question thread for meeting
#5 opened by insightmind - 2
Proposal of LeanInk CLI
#2 opened by insightmind - 0
Setup CI/CD
#4 opened by insightmind