michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(src/emacs/README.md): expand instructions slightly

Browse source
This commit is contained in:
Jeremy Avigad 2015-12-21 16:17:38 -05:00
parent 8d50405e68
commit 68ecdc4c26
1 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/emacs/README.md
View file

@ -132,7 +132,7 @@ lean-mode files are located. With that information, update the
Case 4: Install Lean in Windows Case 4: Install Lean in Windows
------------------------------- -------------------------------
``` ```elisp
;; Set up lean-root path ;; Set up lean-root path
(setq lean-rootdir "\\lean-0.2.0-windows") (setq lean-rootdir "\\lean-0.2.0-windows")
(setq-local lean-emacs-path "\\lean-0.2.0-windows\\share\\emacs\\site-lisp\\lean") (setq-local lean-emacs-path "\\lean-0.2.0-windows\\share\\emacs\\site-lisp\\lean")
@ -140,6 +140,18 @@ Case 4: Install Lean in Windows
(require 'lean-mode) (require 'lean-mode)
``` ```
If things are working correctly, you should see the word ``Lean`` in the
Emacs mode line when you open a file with extension `.lean` (for the
standard Lean mode) or `.hlean` (for hott mode). If you type
```lean
check id
```
the word ``check`` will be underlined, and hovering over it will show
you the type of ``id``. The mode line will show ``FlyC:0/1``, indicating
that there are no errors and one piece of information displayed. Whenever
you type, an asterisk should briefly appear after ``FlyC``, indicating that
your file is being checked.
Key Bindings Key Bindings
============ ============