 (defconst lean-keywords1-regexp
   (eval `(rx word-start (or ,@lean-keywords1) word-end)))
 (defconst lean-keywords2
-  '("by+")
+  '("by+" "begin+")
   "lean keywords ending with 'symbol'")
 (defconst lean-keywords2-regexp
   (eval `(rx word-start (or ,@lean-keywords2) symbol-end)))
 (defconst lean-constants
-  '("#" "@" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨"
+  '("#" "@" "!" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨"
     "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/" "λ"
-    "→" "∃" "∀")
+    "→" "∃" "∀" "∘" "×" "Σ" "Π" "~" "||" "&&" "≃" "≡" "≅"
+    "ℕ" "ℤ" "ℚ" "ℝ" "ℂ" "𝔸"
+    ;; HoTT notation
+    "Ω" "∥" "map₊" "₊" "π₁" "S¹" "⇒" "⟹" "⟶"
+    "⁻¹ᵉ" "⁻¹ᶠ" "⁻¹ᵍ" "⁻¹ʰ" "⁻¹ⁱ" "⁻¹ᵐ" "⁻¹ᵒ" "⁻¹ᵖ" "⁻¹ʳ" "⁻¹ᵛ" "⁻¹ˢ" "⁻²" "⁻²ᵒ"
+    "⬝e" "⬝i" "⬝o" "⬝op" "⬝po" "⬝h" "⬝v" "⬝hp" "⬝vp" "⬝ph" "⬝pv" "⬝r" "◾" "◾o"
+    "∘n" "∘f" "∘fi" "∘nf" "∘fn" "∘n1f" "∘1nf" "∘f1n" "∘fn1"
+    "^c" "≃c" "≅c")
   "lean constants")
 (defconst lean-constants-regexp (regexp-opt lean-constants))
+(defconst lean-numerals-regexp
+  (eval `(rx word-start
+	     (one-or-more digit) (optional (and "." (zero-or-more digit)))
+	     word-end)))
+
 (defconst lean-modifiers
   (--map (s-concat "[" it "]")
          '("persistent" "notation" "visible" "instance" "trans_instance"

      (2 'font-lock-function-name-face))
     ;; place holder
     (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-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)
     ;; tactics
     ("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face))
     (,(rx (not (any "\.")) word-start
           (group
            (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply"
                "apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold" "focus" "focus_at"
                "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
                "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite"
                "xrewrite" "krewrite" "blast" "simp" "esimp" "unfold" "change" "check_expr" "contradiction"
                "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity"
                "symmetry" "transitivity" "state" "induction" "induction_using" "fail" "append"
                "substvars" "now" "with_options"))
           word-end)
      (1 'font-lock-constant-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

           "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr"
           "notations" "abbreviations" "begin_end_hints" "tactic_hints"
           "reduce_hints" "unfold_hints" "aliases" "eqv"
           "localrefinfo" "recursor"))
  "lean modifiers")
(defconst lean-modifiers-regexp
  (regexp-opt lean-modifiers))


(defconst lean-tactics
  '("\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply"
    "apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold" "focus" "focus_at"
    "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
    "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite"
    "xrewrite" "krewrite" "blast" "simp" "esimp" "unfold" "change" "check_expr" "contradiction"
    "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity"
    "symmetry" "transitivity" "state" "induction" "induction_using" "fail" "append"
    "substvars" "now" "with_options")
  "lean tactics")
(defconst lean-tactics-regexp
  (eval `(rx word-start (or ,@lean-tactics) word-end)))


(defconst lean-warnings '("sorry" "exit") "lean warnings")
(defconst lean-warnings-regexp
  (eval `(rx word-start (or ,@lean-warnings) word-end)))


(defconst lean-syntax-table
  (let ((st (make-syntax-table)))
