lean4-mode
lean4-mode copied to clipboard
leanprover-community
Emacs major mode for Lean 4
This allows one to press on the link to go to the corresponding file/line/column. Screenshot attached, where the section headers are now clickable links, that take one to the correct...
Is it possible to bundle evil keybindings into this package? I made some keybindings for the existing commands (doomemacs) ```emacs-lisp (map! :after lean4-mode :localleader :map lean4-mode-map :desc "Execute" "R" #'lean4-execute...
In this screenshot, the highlighting of `dbgTraceIfShared` is a bit funky:  It seems to me that the issue comes from [here](https://github.com/leanprover/lean4-mode/blob/2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440/lean4-syntax.el#L47-L48), where there is no `word-end` in the `rx`...
The option to collapse/expand trace nodes is extremely helpful when navigating e.g. typeclass synthesis traces. But at least with my setup (Doom Emacs + lean4-mode), the traces are always fully...
Per [this zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lean4-mode.20with.20nix-doom-emacs/near/291790287) on nix-specific papercuts in packaging lean4-mode for (doom-)emacs. I've erred on the side of being verbose; plausibly lines 52-69 are really all that's needed in the...
I think the VS code extension has a pause button on the info buffer. I couldn't find this functionality, so added some quick and dirty advice to accomplish the same...
