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


(defun fstar-setup-fontlock ()
  "Setup font-lock for use with F*."
  (font-lock-add-keywords
   nil `((,fstar-syntax-constants . 'font-lock-constant-face)
         (,fstar-syntax-keywords  . 'font-lock-keyword-face)
         (,fstar-syntax-builtins  . 'font-lock-builtin-face)
         (,fstar-syntax-structure . 'tuareg-font-lock-governing-face)
         ,@fstar-syntax-additional)))

(define-derived-mode fstar-mode tuareg-mode "F✪"
  (fstar-setup-prettify)
  (fstar-setup-fontlock))

(add-to-list 'auto-mode-alist '("\\.fst\\'" . fstar-mode))



;; Copyright (C) 2015 Clément Pit--Claudel
;; Author: Clément Pit--Claudel <clement.pitclaudel@live.com>
;; URL: https://github.com/FStarLang/fstar.el

;; Created: 27 Aug 2015
;; Version: 0.1
;; Package-Requires: ((flycheck "0.25") (emacs "24.3"))
;; Keywords: convenience, languages

;; This file is not part of GNU Emacs.

;; This program is free software: you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or
;; (at your option) any later version.

;; This program is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.

;; You should have received a copy of the GNU General Public License
;; along with this program.  If not, see <http://www.gnu.org/licenses/>.

;;; Commentary:

