issues
search
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
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Error when analyzing a simple file with `LeankInk`: `failed to read file ..., invalid header`
#59
mariovagomarzal
opened
1 month ago
0
fix: handle lakefile.toml
#58
gaetanserre
closed
1 month ago
1
chore: bump for lean4#3159
#57
mhuisi
closed
7 months ago
0
Using `Mathlib` as an import causes `leanInk` to error
#56
femtomc
opened
8 months ago
0
fix: `print-paths` changed to `setup-file` in Lean v4.4.0
#55
utensil
closed
8 months ago
4
chore: bump to nightly-2023-08-19
#54
semorrison
closed
1 year ago
0
chore: clean up unused arguments
#53
semorrison
closed
1 year ago
0
chore: bump to nightly-2023-04-11
#52
semorrison
closed
1 year ago
0
chore: pin a Mathlib commit for tests
#51
semorrison
closed
1 year ago
0
chore: correct some paths
#50
semorrison
closed
1 year ago
0
chore: normalize whitespace
#49
semorrison
closed
1 year ago
0
chore: bump to nightly-2023-08-19
#48
semorrison
closed
1 year ago
3
Reduction
#47
0art0
closed
1 year ago
0
Creating a bare-bones `LeanInk`
#46
0art0
closed
1 year ago
1
Removes duplicate bubbles after comment
#45
vanessa-rodrigues
closed
1 year ago
0
Removes duplicate bubbles after comment
#44
vanessa-rodrigues
closed
1 year ago
0
chore: bump lean
#43
gebner
closed
1 year ago
0
Adds flags to control Alectryon output
#42
vanessa-rodrigues
closed
1 year ago
1
Bump lean version
#41
0art0
closed
1 year ago
1
chore: rename `le_or_eq_or_le_succ`
#40
chabulhwi
closed
1 year ago
0
doc-gen fork merge
#39
hargoniX
closed
1 month ago
0
fix typo in AppInfo description
#38
hrmacbeth
opened
1 year ago
0
fix: snake-case attributes
#37
digama0
closed
1 year ago
0
chore: adapt to impl-detail hyps
#36
gebner
closed
1 year ago
1
We need to get back the "Copy to clipboard" button on Lean code snippets
#35
lovettchris
opened
1 year ago
0
Red squiggles
#34
lovettchris
opened
2 years ago
0
monadic commands
#33
lovettchris
closed
1 year ago
2
We need to get back the "Try It" button when manual is read inside VS code documentation view
#32
lovettchris
opened
2 years ago
0
Switch to using Lean to run the tests (so it runs on Windows)
#31
lovettchris
closed
2 years ago
1
Provide the mdbook `# namespace hidden` trick
#30
lovettchris
opened
2 years ago
1
Provide a way to tell leanink to generate comments on #eval, #check commands
#29
lovettchris
opened
2 years ago
2
fix: code review feedback from Mac.
#28
lovettchris
closed
2 years ago
1
Error with custom notation
#27
lecopivo
closed
2 years ago
4
fix: update to latest version of lean, and fix the lakefile.lean
#26
lovettchris
closed
2 years ago
2
Hiding certain Lean imports at the beginging of a chapter
#25
lovettchris
opened
2 years ago
0
LeanInk silently eats lean compile errors
#24
lovettchris
opened
2 years ago
1
LeanInk has trouble with infix operators
#23
lovettchris
opened
2 years ago
0
Colorization difference
#22
lovettchris
opened
2 years ago
0
LeanInk can't install itself for brew-installed elan
#21
utensil
opened
2 years ago
10
nix: Undefined symbols for architecture since #16
#20
ConnorBaker
closed
2 years ago
3
Fix test suite
#19
Kha
closed
2 years ago
2
feat: support for custom user extensions
#18
hargoniX
closed
2 years ago
5
Update lean-toolchain and CLI improvements
#17
insightmind
closed
2 years ago
1
Move Main to top level
#16
xubaiw
closed
2 years ago
4
No types or goals inside matches
#15
Kha
closed
2 years ago
2
Update Lean & minor fix
#14
Kha
closed
2 years ago
0
Wrong Typename exported
#13
insightmind
closed
2 years ago
0
Extract type information from info tree
#12
insightmind
closed
2 years ago
0
Alectryon Type Information on hover
#11
insightmind
closed
2 years ago
0
Lean 4 syntax highlighting in Alectryon
#10
insightmind
closed
2 years ago
0
Next