diff --git a/doc/highlight.js b/doc/highlight.js index 2a184e9e82..af943fabea 100644 --- a/doc/highlight.js +++ b/doc/highlight.js @@ -1115,7 +1115,7 @@ hljs.registerLanguage("lean", function(hljs) { 'import open export theory prelude renaming hiding exposing ' + 'calc match with do by let extends ' + 'for in unless try catch finally mutual mut return continue break where rec ' + - 'syntax macro_rules macro ' + + 'syntax macro_rules macro deriving ' + 'fun ' + '#check #check_failure #eval #reduce #print ' + 'section namespace end infix infixl infixr postfix prefix ', diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el index 439b516842..12343cbc85 100644 --- a/lean4-mode/lean4-syntax.el +++ b/lean4-mode/lean4-syntax.el @@ -20,7 +20,7 @@ "try" "catch" "finally" "where" "rec" "mut" "forall" "fun" "exists" "if" "then" "else" "from" "init_quot" "return" "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro" "scoped" - "initialize" "builtin_initialize" "induction" "cases" "generalizing" "unif_hint") + "initialize" "builtin_initialize" "induction" "cases" "generalizing" "unif_hint" "deriving") "lean keywords ending with 'word' (not symbol)") (defconst lean4-keywords1-regexp (eval `(rx word-start (or ,@lean4-keywords1) word-end)))