lean-mode
lean-mode copied to clipboard
leanprover
Emacs mode for Lean
When installing lean-mode from elpa, I get the following error: `In helm-lean-definitions: helm-lean.el:47:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)` This may cause...
When writing a multi-line comment like ```lean /-- Line 1 Line 2 ... -/ ``` Suppose the user types in `/---/` and places the cursor before the last `-`. Pressing...
Hi, when I create a .lean file, Emacs shows me the following message: "lean scroll hook: (error Lean was not found in the ’exec-path’ and ’lean-rootdir’ is not defined. Please...
I searched the functions provided by the mode and `lean-toggle-flycheck-mode` appears to be the intended way to disable flycheck, but whenever I toggle it (either manually or via hook) lean-mode...
Hi, I'm newbie about this proof assistant and at the same time avid emacs user. I want to learn Lean for my control system research. I thought it would be...
I get this error: ``` error: type must be string, but is null [3 times] ``` it seems like lean insists on sending buffer file names that are null: ```...
mirroring https://github.com/flycheck/flycheck/issues/302 when using vanilla flycheck, doing ```elisp (setq flycheck-display-errors-function #'flycheck-display-error-messages-unless-error-list) ``` solves this issue. however from my understanding of the code `lean-mode` is handling error display manually, and the...
During classes, I would like to increase the size of the fonts in the minibuffer so students can see the types in the cursor position. Any idea? Using the code...
http://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf slide 5 says I can have a type of a subterm if I put a cursor on the open-paren. it is not working for me. Any idea? Emacs 26.1....
Hi, I created a simple project to test out `mathlib`. It was working initially but revisiting the test file later, I got an error message: > Warning (flycheck): Syntax checker...
