 
 (require 'rx)
 
-(defconst lean-keywords
+(defconst lean-keywords1
   '("import" "prelude" "tactic_hint" "protected" "private" "noncomputable" "definition" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"

     ;; place holder
     (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
     ;; modifiers
     (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[trans-instance\]" "\[class\]" "\[parsing-only\]"
               "\[coercion\]" "\[unfold-full\]" "\[constructor\]" "\[reducible\]"
               "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]"
               "\[whnf\]" "\[multiple-instances\]" "\[none\]"
               "\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]"
               "\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" "\[simp\]" "\[congr\]"
               "\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]"
               "\[reduce-hints\]" "\[unfold-hints\]" "\[aliases\]" "\[eqv\]" "\[localrefinfo\]"))
      . 'font-lock-doc-face)
     (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
     (,(rx "\[recursor" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
     (,(rx "\[unfold" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)

     ;; Types
     (,(rx word-start (or "Prop" "Type" "Type'" "Type₊" "Type₀" "Type₁" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face)
     (,(rx word-start (group "Type") ".") (1 'font-lock-type-face))
     ;; warnings
     (,lean-warnings-regexp . 'font-lock-warning-face)
     ;; extra-keywords
     (,(rx (or "∎")) . 'font-lock-keyword-face))))

;; Syntax Highlighting for Lean Info Mode
(defconst lean-info-font-lock-defaults
