max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(frontends/lean/decl_cmds,emacs/lean-syntax): typo

Browse source
This commit is contained in:
Gabriel Ebner 2017-08-28 17:04:03 +02:00
parent 9920062b69
commit 05178ad950
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/emacs/lean-syntax.el
View file

@ -130,7 +130,7 @@
(1 'font-lock-doc-face))
(,(rx (group "#" (or "eval" "print" "reduce" "help" "check")))
(1 'font-lock-keyword-face))
;; mutal definitions "names"
;; mutual definitions "names"
(,(rx word-start
"mutual"
word-end

2
src/frontends/lean/decl_cmds.cpp
View file

@ -559,7 +559,7 @@ void register_decl_cmds(cmd_table & r) {
add_cmd(r, cmd_info("constants", "declare new constants (aka top-level variables)", constants_cmd));
add_cmd(r, cmd_info("axioms", "declare new axioms", axioms_cmd));
add_cmd(r, cmd_info("meta", "add new meta declaration", modifiers_cmd, false));
add_cmd(r, cmd_info("mutual", "add new mutal declaration", modifiers_cmd, false));
add_cmd(r, cmd_info("mutual", "add new mutual declaration", modifiers_cmd, false));
add_cmd(r, cmd_info("noncomputable", "add new noncomputable definition", modifiers_cmd, false));
add_cmd(r, cmd_info("private", "add new private declaration", modifiers_cmd, false));
add_cmd(r, cmd_info("protected", "add new protected declaration", modifiers_cmd, false));