 ;;; Prettify symbols
 
 (defconst fstar-symbols-alist '(("exists" . ?∃) ("forall" . ?∀) ("fun" . ?λ)
-                            ("nat" . ?ℕ) ("int" . ?ℤ)
-                            ("True" . ?⊤) ("False" . ?⊥)
-                            ("*" . ?×) ("~>" . ?↝)
-                            ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
-                            ("/\\" . ?∧) ("\\/" . ?∨) ("~" . ?¬) ("<>" . ?≠)
-                            ;; ("&&" . ?∧) ("||" . ?∨) ("=!=" . ?≠)
-                            ("<==>" . ?⟺) ("==>" . ?⟹)
-                            ("=>" . ?⇒) ("->" . ?→)
-                            ;; ("(|" . 10629) ("|)" . 10630)
-                            ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
-                            ("'d" . ?δ) ("'e" . ?ϵ))
+                           ("nat" . ?ℕ) ("int" . ?ℤ)
+                           ("True" . ?⊤) ("False" . ?⊥)
+                           ("*" . ?×) ("~>" . ?↝)
+                           ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
+                           ("/\\" . ?∧) ("\\/" . ?∨) ("~" . ?¬) ("<>" . ?≠)
+                           ;; ("&&" . ?∧) ("||" . ?∨) ("=!=" . ?≠)
+                           ("<==>" . ?⟺) ("==>" . ?⟹)
+                           ("=>" . ?⇒) ("->" . ?→)
+                           ;; ("(|" . 10629) ("|)" . 10630)
+                           ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
+                           ("'d" . ?δ) ("'e" . ?ϵ))
   "Fstar symbols.")
 
 (defun fstar-setup-prettify ()


(provide 'fstar-mode)
;;; fstar-mode.el ends here

;; Local Variables:
;; nameless-aliases: (("f*" . "fstar"))
;; End:

       (1 'fstar-structure-face)
       (2 'font-lock-function-name-face)
       (fstar-find-id (fstar-subexpr-pre-matcher 2) nil
                 (1 'font-lock-variable-name-face)))
      (fstar-find-id-with-type
       (1 'font-lock-variable-name-face))
      (,(concat "\\_<\\(type\\|kind\\)\\( +" id "\\)\\s-*$")
