diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el
index 010b89b13..2ff647407 100644
--- a/src/emacs/lean-info.el
+++ b/src/emacs/lean-info.el
@@ -588,9 +588,10 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
              ", ")))
     (when extra
       (setq str
-            (format "(%s) : %s"
-                    (propertize (lean-info-extra-expr-str extra) 'face 'font-lock-variable-name-face)
-                    (lean-info-extra-type-str extra))))
+            (cond (lean-show-only-type-in-parens (format ": %s" (lean-info-extra-type-str extra)))
+                  (t (format "(%s) : %s"
+                             (propertize (lean-info-extra-expr-str extra) 'face 'font-lock-variable-name-face)
+                             (lean-info-extra-type-str extra))))))
     (when (and name-str type-str)
       (setq str (format "%s : %s"
                         (propertize name-str 'face 'font-lock-variable-name-face)
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index 78badc556..10ef6af29 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -60,6 +60,10 @@
   "lean-flychecker checker option"
   :group 'lean)
 
+(defcustom lean-show-only-type-in-parens t
+  "Show only types of expression in parens if non-nil. Otherwise,
+show both of expressions and types.")
+
 (defcustom lean-delete-trailing-whitespace nil
   "Set this variable to true to automatically delete trailing
 whitespace when a buffer is loaded from a file or when it is