2014-08-07 15:03:49 +00:00
|
|
|
lean-mode
|
|
|
|
|
=========
|
|
|
|
|
|
2014-08-07 17:37:25 +00:00
|
|
|
Emacs mode for [lean theorem prover][lean]
|
|
|
|
|
|
|
|
|
|
[lean]: https://github.com/leanprover/lean
|
|
|
|
|
|
2014-08-07 15:03:49 +00:00
|
|
|
Requirement
|
|
|
|
|
-----------
|
|
|
|
|
|
2014-08-07 17:37:25 +00:00
|
|
|
``lean-mode`` requires [Emacs 24][emacs24] and following (optional)
|
2014-08-14 00:02:49 +00:00
|
|
|
packages which can be installed via <kbd>M-x package-install</kbd>.
|
2014-08-07 17:37:25 +00:00
|
|
|
|
2014-08-25 23:51:23 +00:00
|
|
|
- [dash][dash]
|
|
|
|
|
- [dash-functional][dash]
|
2014-08-07 15:03:49 +00:00
|
|
|
- [flycheck][flycheck]
|
|
|
|
|
- [fill-column-indicator][fci]
|
2014-08-07 17:37:25 +00:00
|
|
|
- [whitespace-cleanup-mode][wcm]
|
|
|
|
|
|
|
|
|
|
To install them, you need to have [MELPA][MELPA] in your
|
|
|
|
|
``package-archives``. You can add it by evaluating the following elisp
|
|
|
|
|
code:
|
|
|
|
|
|
|
|
|
|
```elisp
|
|
|
|
|
(add-to-list 'package-archives
|
|
|
|
|
'("marmalade" . "http://marmalade-repo.org/packages/") t)
|
|
|
|
|
```
|
2014-08-07 15:03:49 +00:00
|
|
|
|
2014-08-25 23:51:23 +00:00
|
|
|
[emacs24]: http://www.gnu.org/software/emacs
|
|
|
|
|
[flycheck]: http://flycheck.readthedocs.org/en/latest
|
2014-08-07 15:03:49 +00:00
|
|
|
[fci]: https://github.com/alpaker/Fill-Column-Indicator
|
2014-08-07 17:37:25 +00:00
|
|
|
[wcm]: https://github.com/purcell/whitespace-cleanup-mode
|
2014-08-25 23:51:23 +00:00
|
|
|
[MELPA]: http://melpa.milkbox.net
|
|
|
|
|
[dash]: https://github.com/magnars/dash.el
|
2014-08-07 15:03:49 +00:00
|
|
|
|
|
|
|
|
Setup
|
|
|
|
|
-----
|
|
|
|
|
|
2014-08-07 17:37:25 +00:00
|
|
|
Put the following elisp code on your emacs setup:
|
|
|
|
|
|
2014-08-07 15:03:49 +00:00
|
|
|
```elisp
|
|
|
|
|
(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)
|
|
|
|
|
|
2014-08-07 17:37:25 +00:00
|
|
|
;; lean customization
|
2014-08-07 15:03:49 +00:00
|
|
|
(customize-set-variable 'lean-show-rule-column-method 'vline)
|
|
|
|
|
(customize-set-variable 'lean-rule-column 100)
|
2014-08-07 18:57:46 +00:00
|
|
|
(customize-set-variable 'lean-rule-color "#ff0000")
|
2014-08-07 15:03:49 +00:00
|
|
|
(customize-set-variable 'lean-delete-trailing-whitespace t)
|
|
|
|
|
```
|
2014-08-15 00:10:58 +00:00
|
|
|
|
|
|
|
|
Key Bindings
|
|
|
|
|
------------
|
|
|
|
|
|
|
|
|
|
|Key | Function |
|
|
|
|
|
|-------------------|-----------------------------------|
|
|
|
|
|
|<kbd>C-c C-x</kbd> | lean-std-exe |
|
|
|
|
|
|<kbd>C-c C-l</kbd> | lean-std-exe |
|
|
|
|
|
|<kbd>C-c C-t</kbd> | lean-eldoc-documentation-function |
|
|
|
|
|
|<kbd>C-c C-f</kbd> | lean-fill-placeholder |
|
2014-08-16 03:48:30 +00:00
|
|
|
|<kbd>M-.</kbd> | lean-find-tag |
|
2014-08-16 04:23:36 +00:00
|
|
|
|<kbd>TAB</kbd> | lean-complete-tag |
|
2014-08-25 23:51:23 +00:00
|
|
|
|<kbd>C-c C-o</kbd> | lean-set-option |
|
|
|
|
|
|<kbd>C-c C-e</kbd> | lean-eval-cmd |
|
