lean4-mode
lean4-mode copied to clipboard
leanprover-community
Emacs major mode for Lean 4
I prefer to use the eglot language server implementation over `lsp-mode`. It would be nice to have an option to set which language server to use, or to make the...
Contrary to most major modes, syntax highlighting in `lean4-mode` is not instantaneous, in the sense that if I start typing `def a : Nat :=`, it won't syntax highlight until...
I also encountered #36 and decided to give it a try. ### How the bug was introduced The original code was added in https://github.com/leanprover/lean4/commit/ba4fdce508351bb222e58769fa1ce19a938a1f96 , where you can see `(defconst...
I have installed Lean4 via `elan` and have set `lean-rootdir` to `home/cla/.elan` and then `home/cla/.elan/` and both times when I try to use `lean-toggle-show-goal` with the default Main.lean file generated...
In #51, @akirak made some suggestions that were deemed out of the scope of that PR. Go over these suggestions and decide whether to implement them.
Use named sections so magit-section can track which sections are expanded. Don't use sections for individual diagnostics, since they can't be tracked. Capture data in lexicals for deferred rendering by...
For some reason even though there is a ton of space the text that tells you what the result of the #check directive is decides to wrap around. I'm using...
Per the [ `nix-doom-emacs` install instructions thread]https://github.com/leanprover/lean4-mode/issues/15#issuecomment-1156172981), I'd like to request that `lean4-mode` be added to `melpa`.
Lean (version 4.4.0, commit ca7d6dadb9e1, Release) lean4-mode commit: d1c9364 GNU Emacs 28.1 (build 1, x86_64-pc-linux-gnu, GTK+ Version 3.24.20, cairo version 1.16.0) of 2022-05-31 ``` Debugger entered--Lisp error: (error "The connected...
I'm not sure if I've done something wrong or if the installation instructions could be made a little more explicit. Currently, my environment is: 1. NixOS 22.05 (just upgraded today),...