a08ad99dba
Close #99 |
||
---|---|---|
.. | ||
CMakeLists.txt | ||
eri.el | ||
lean-cmd.el | ||
lean-company.el | ||
lean-debug.el | ||
lean-flycheck.el | ||
lean-info.el | ||
lean-input.el | ||
lean-mode.el | ||
lean-option.el | ||
lean-server.el | ||
lean-settings.el | ||
lean-syntax.el | ||
lean-tags.el | ||
lean-type.el | ||
lean-util.el | ||
lean-variable.el | ||
README.md |
lean-mode
Emacs mode for lean theorem prover
Requirement
lean-mode
requires Emacs 24 and following (optional)
packages which can be installed via M-x package-install.
Install
Put the following elisp code on your emacs setup (e.g. .emacs.d/init.el
):
(require 'package)
(add-to-list 'package-archives
'("melpa" . "http://melpa.milkbox.net/packages/") t)
(package-initialize)
(package-refresh-contents)
;; Install required packages for lean-mode
(defvar lean-mode-required-packages
'(company dash dash-functional flycheck whitespace-cleanup-mode fill-column-indicator))
(dolist (p lean-mode-required-packages)
(when (not (package-installed-p p))
(package-install p)))
;; Set up lean-root path
(setq lean-rootdir "~/projects/lean")
(setq-local lean-emacs-path
(concat (file-name-as-directory lean-rootdir)
(file-name-as-directory "src")
"emacs"))
(add-to-list 'load-path (expand-file-name lean-emacs-path))
(require 'lean-mode)
;; Customization for lean-mode
(customize-set-variable 'lean-delete-trailing-whitespace t)
(customize-set-variable 'lean-flycheck-use t)
(customize-set-variable 'lean-eldoc-use t)
Key Bindings
Key | Function |
---|---|
C-c C-x | lean-std-exe |
C-c C-l | lean-std-exe |
C-c C-t | lean-eldoc-documentation-function |
C-c C-f | lean-fill-placeholder |
M-. | lean-find-tag |
TAB | lean-complete-tag |
C-c C-o | lean-set-option |
C-c C-e | lean-eval-cmd |