leanprover lean3-mode issues

leanprover / lean3-mode

Emacs mode for Lean

Apache License 2.0

69 stars 17 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Naming of lean-mode and lean4-mode

#48 mekeor closed 3 months ago
1
Compiling helm-lean yields docstring error

#47 rommeswi opened 1 year ago
1
Fix #45.

#46 jmbr closed 1 year ago
0
Error loading lean-mode in GNU Emacs 30.0.50

#45 jmbr closed 1 year ago
0
Lean the mode

#44 sirikid closed 1 year ago
1
Difficulty writing multi-line comments due to autocompletion

#43 lenianiva opened 1 year ago
0
Prevent lean-server from complaining when disabling flycheck

#42 kozytskyiad opened 2 years ago
0
Add weakly covers symbol and opposites shortcuts

#41 YaelDillies closed 2 years ago
0
Add covers symbol and blackboard letters

#40 YaelDillies closed 2 years ago
0
Add `\specializes →` ⤳ abbreviation

#39 erdOne closed 2 years ago
0
Abbreviations `\/` and `\quot` for `⧸`

#38 Vierkantor closed 2 years ago
0
Add some quality of life changes

#37 Zetagon closed 3 years ago
3
lean server sync: (json-readtable-error 99)

#36 Alf0nso closed 3 years ago
1
Incorporate in org mode -- implement ob-lean

#35 HyunggyuJang opened 3 years ago
0
feat(*): port to eldoc handling of emacs 28

#34 kritixilithos closed 3 years ago
0
Porting to emacs 28's newer eldoc versions

#33 kritixilithos closed 3 years ago
1
Replace deprecated dash-functional dependency

#32 basil-conto closed 3 years ago
0
chore: require lean-info in lean-type

#31 collares closed 3 years ago
0
Make sure each file byte-compiles by itself with no errors

#30 collares closed 4 years ago
1
Change functor arrow to rightwards harpoon

#29 kmill closed 3 years ago
0
Clarifying the readme, and a typo

#28 kmill closed 4 years ago
0
Reuse the window for info buffers

#27 kmill closed 4 years ago
1
Change the requires-pattern in helm-lean

#26 kmill closed 4 years ago
0
Modified overlays for the message boxes

#25 kmill closed 4 years ago
1
Increase memory limit for lean from 1G to 4G

#24 anrddh closed 4 years ago
0
Allow displaying Lean goal in another frame

#23 iocta closed 4 years ago
1
feat(lean-input): update

#22 fpvandoorn closed 4 years ago
0
fix(lean-eri): require cl-lib

#21 kritixilithos closed 4 years ago
1
Indentation does not appear to work

#20 kritixilithos closed 4 years ago
5
Dependency problem on installation

#19 dde-cls closed 5 years ago
1
fix(lean-eri): remove runtime require of cl

#18 bandali0 closed 5 years ago
1
"error: type must be string, but is null"

#17 rgrinberg opened 5 years ago
0
build fails on 5.2.6-arch1-1-ARCH

#16 ghost closed 5 years ago
1
Problems with exec-path and lean-rootdir

#15 oliveira-caio opened 5 years ago
7
Don't Display Current Flycheck Message in Minibuffer when *Flycheck Errors* Buffer is Visible

#14 odanoburu opened 5 years ago
0
font-size in the mini buffer messages

#13 arademaker opened 6 years ago
0
show type

#12 arademaker opened 6 years ago
1
Please mention M-, in the list of keybindings in the README

#11 dagit closed 6 years ago
0
feature request: Please expose lean-message-boxes-enabledp as defcustom

#10 dagit closed 6 years ago
0
feat(lean-diff-types): take type diff from `company-coq`

#9 cipher1024 closed 6 years ago
3
wrong lean version used? -- "Syntax checker lean-checker reported too many errors"

#8 holtzermann17 opened 6 years ago
0
filling block comments produces "unexpected end of comment block" error

#7 holtzermann17 closed 6 years ago
3
fix(lean-info): `lean-show-goal` no longer interrupts `lean-find-defi…

#6 cipher1024 closed 6 years ago
2
Default to executable name "lean"

#5 cdunham closed 6 years ago
1
(json-unknown-keyword fish)

#4 fusiongyro closed 6 years ago
3
lean-mode-required-packages variable

#3 arademaker closed 7 years ago
1
chore(README): clarifications

#2 Kha closed 7 years ago
1
Update README instructions for using MELPA

#1 jroesch closed 7 years ago
2