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

feat(emacs): highlight 'inversion' tactic

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-27 10:26:32 -08:00
parent db9fd53b80
commit f8fa9f3344
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -123,7 +123,7 @@
(,(rx (not (any "\.")) word-start
(or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "rename" "intro" "intros"
"generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat"
"whnf" "rotate" "rotate_left" "rotate_right")
"whnf" "rotate" "rotate_left" "rotate_right" "inversion")
word-end)
. 'font-lock-constant-face)
;; Types