lean2/src/emacs
Soonho Kong 99e77db8ad feat(emacs/lean-flycheck): override flycheck-try-parse-error-with-pattern
For lean-mode, we override flycheck-try-parse-error-with-pattern to
increase column number by 1. It uses defadvice.
2014-08-14 11:21:09 -07:00
..
CMakeLists.txt feat(emacs): include lean-mode Emacs files in the distribution 2014-01-09 11:50:07 -08:00
lean-cmd.el feat(emacs): implement lean-show-type 2014-08-13 17:02:49 -07:00
lean-debug.el feat(emacs): implement lean-show-type 2014-08-13 17:02:49 -07:00
lean-flycheck.el feat(emacs/lean-flycheck): override flycheck-try-parse-error-with-pattern 2014-08-14 11:21:09 -07:00
lean-info.el fix(emacs): add and use lean-string-join 2014-08-14 08:42:52 -07:00
lean-input.el feat(library/hott): add basic HoTT definitions and theorems 2014-07-15 21:46:33 +01:00
lean-mode.el feat(emacs): show overload information 2014-08-14 07:23:15 -07:00
lean-server.el feat(emacs/lean-server.el): add lean-server-{kill,restart}-process 2014-08-14 08:56:46 -07:00
lean-settings.el feat(emacs): implement lean-show-type 2014-08-13 17:02:49 -07:00
lean-type.el fix(emacs): add and use lean-string-join 2014-08-14 08:42:52 -07:00
lean-util.el fix(emacs): add and use lean-string-join 2014-08-14 08:42:52 -07:00
lean-variable.el feat(emacs): implement lean-show-type 2014-08-13 17:02:49 -07:00
README.md feat(emacs): implement lean-show-type 2014-08-13 17:02:49 -07:00

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.

To install them, you need to have MELPA in your package-archives. You can add it by evaluating the following elisp code:

(add-to-list 'package-archives
             '("marmalade" . "http://marmalade-repo.org/packages/") t)

Setup

Put the following elisp code on your emacs setup:

(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)

;; lean customization
(customize-set-variable 'lean-show-rule-column-method 'vline)
(customize-set-variable 'lean-rule-column 100)
(customize-set-variable 'lean-rule-color "#ff0000")
(customize-set-variable 'lean-delete-trailing-whitespace t)