diff --git a/src/emacs/lean-project.el b/src/emacs/lean-project.el
index 1ace370012..cfb7564cee 100644
--- a/src/emacs/lean-project.el
+++ b/src/emacs/lean-project.el
@@ -16,25 +16,32 @@
 (defun lean-project-inside-p ()
   (if (lean-project-find-root) t nil))
 
-(defun lean-project-create (directory)
+(defun lean-project-create (directory type)
   (interactive
-   (list (read-directory-name "Specify the project root directory: ")))
+   (list (read-directory-name "Specify the project root directory: ")
+         (intern (completing-read "Project type:: " '(standard hott)))))
   (let ((project-file (concat (file-name-as-directory directory)
-                               lean-project-file-name)))
+                              lean-project-file-name))
+        (ext (pcase type
+               (`standard "lean")
+               (`hott     "hlean")))
+        (default-contents
+          (s-join "\n"
+                  ;;  EXT is a placeholder.
+                  '("# Lean project file"
+                    ""
+                    "# Include all .EXT files under this directory"
+                    "+ *.EXT"
+                    ""
+                    "# Exclude flycheck generated temp files"
+                    "- flycheck*.EXT"
+                    ""
+                    "# Exclude emacs temp files"
+                    "- .#*.EXT"))))
     (if (file-exists-p project-file)
         (user-error "project-file %s already exists" project-file))
     (find-file project-file)
-    (insert (s-join "\n"
-                    '("# Lean project file"
-                      ""
-                      "# Include all .lean files under this directory"
-                      "+ *.lean"
-                      ""
-                      "# Exclude flycheck generated temp files"
-                      "- flycheck*.lean"
-                      ""
-                      "# Exclude emacs temp files"
-                      "- .#*.lean")))
+    (insert (s-replace "EXT" ext default-contents))
     (save-buffer)))
 
 (provide 'lean-project)