From 82dc155f0ffe5f3ab76c47063f110ba645f58844 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Oct 2020 15:09:17 -0700 Subject: [PATCH] chore: add `builtin_initialize` 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 c237b1e8a9..9c752b9a0b 100644 --- a/lean4-mode/lean4-syntax.el +++ b/lean4-mode/lean4-syntax.el @@ -22,7 +22,7 @@ "try" "catch" "finally" "where" "rec" "forall" "Pi" "fun" "exists" "if" "then" "else" "assume" "from" "init_quot" "return" "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro" - "initialize") + "initialize" "builtin_initialize") "lean keywords ending with 'word' (not symbol)") (defconst lean4-keywords1-regexp (eval `(rx word-start (or ,@lean4-keywords1) word-end)))