From be730fa27f2b8fcf55f9e6bb51ad9f6fdc716ebd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Feb 2020 12:52:51 -0800 Subject: [PATCH] feat: add `#check_failure` as keyword --- lean4-mode/lean4-syntax.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el index 57c900519e..79617c5199 100644 --- a/lean4-mode/lean4-syntax.el +++ b/lean4-mode/lean4-syntax.el @@ -127,7 +127,7 @@ (1 'font-lock-doc-face)) (,(rx (group "@[" (zero-or-more (not (any "]"))) "]")) (1 'font-lock-doc-face)) - (,(rx (group "#" (or "eval" "print" "reduce" "help" "check" "synth"))) + (,(rx (group "#" (or "eval" "print" "reduce" "help" "check" "check_failure" "synth"))) (1 'font-lock-keyword-face)) ;; mutual definitions "names" (,(rx word-start