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

Issues: leanprover/lean3-mode

10 Open 13 Closed
10 Open 13 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

Compiling helm-lean yields docstring error
#47 opened Oct 11, 2023 by rommeswi
1
Difficulty writing multi-line comments due to autocompletion
#43 opened Mar 15, 2023 by lenianiva
Prevent lean-server from complaining when disabling flycheck
#42 opened Aug 1, 2022 by kozytskyiad
Incorporate in org mode -- implement ob-lean
#35 opened Apr 13, 2021 by HyunggyuJang
"error: type must be string, but is null"
#17 opened Sep 7, 2019 by rgrinberg
Problems with exec-path and lean-rootdir
#15 opened Jul 22, 2019 by oliveira-caio
7
Don't Display Current Flycheck Message in Minibuffer when *Flycheck Errors* Buffer is Visible
#14 opened Nov 27, 2018 by odanoburu
font-size in the mini buffer messages
#13 opened Oct 25, 2018 by arademaker
show type
#12 opened Oct 25, 2018 by arademaker
1
wrong lean version used? -- "Syntax checker lean-checker reported too many errors"
#8 opened Jul 24, 2018 by holtzermann17
ProTip! Exclude everything labeled bug with -label:bug.