diff --git a/src/emacs/README.md b/src/emacs/README.md index 1c461faeaa..f8fec9a530 100644 --- a/src/emacs/README.md +++ b/src/emacs/README.md @@ -156,18 +156,18 @@ Key Bindings and Commands |Key | Function | |-------------------|-------------------------------------------------------------------------------| -|M-. | jump to definition in source file (lean-find-tag) | -|TAB | tab complete identifier, option, filename, etc. (lean-tab-indent-or-complete) | +# |M-. | jump to definition in source file (lean-find-tag) | +# |TAB | tab complete identifier, option, filename, etc. (lean-tab-indent-or-complete) | |C-c C-k | shows the keystroke needed to input the symbol under the cursor | |C-c C-g | show goal in tactic proof (lean-show-goal-at-pos) | |C-c C-p | print information about identifier (lean-show-id-keyword-info) | -|C-c C-t | show type (lean-show-type) | -|C-c C-f | replace underscore by inferred value (lean-fill-placeholder) | +# |C-c C-t | show type (lean-show-type) | +# |C-c C-f | replace underscore by inferred value (lean-fill-placeholder) | |C-c C-x | execute lean in stand-alone mode (lean-std-exe) | |C-c C-l | execute lean in stand-alone mode (lean-std-exe) | |C-c C-o | set option (lean-set-option) | -|C-c C-r | restart lean process (lean-server-reset-process) | -|C-c C-e | evaluate a lean comman (lean-eval-cmd) | +|C-c C-e | evaluate a lean command (lean-eval-cmd) | +|C-c C-n | toggle next-error-mode: shows next error in dedicated lean-info buffer | |C-c ! n | flycheck: go to next error | |C-c ! p | flycheck: go to previous error | |C-c ! l | flycheck: show list of errors |