diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index f71056a547..fd14cb77e6 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -87,7 +87,7 @@
   (local-set-key "\C-c\C-l"  'lean-std-exe)
   (local-set-key "\C-c\C-o"  'lean-set-option)
   (local-set-key "\C-c\C-e"  'lean-eval-cmd)
-  (local-set-key "\C-c\C-t"  'lean-eldoc-documentation-function)
+  (local-set-key "\C-c\C-t"  'lean-show-type)
   (local-set-key "\C-c\C-f"  'lean-fill-placeholder)
   (local-set-key "\M-."      'lean-find-tag)
   (local-set-key (kbd "TAB") 'lean-tab-indent-or-complete))
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index 54ea8f3fb9..b8864c07f0 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -122,4 +122,11 @@ written."
   :type 'sexp
   :risky t)
 
+(defcustom lean-show-type-add-to-kill-ring nil
+  "If it is non-nil, add the type information to the kill-ring so
+that user can yank(paste) it later. By default, it's
+false (nil)."
+  :group 'lean
+  :type 'boolean)
+
 (provide 'lean-settings)
diff --git a/src/emacs/lean-type.el b/src/emacs/lean-type.el
index cb24a00ea8..2ce6f6fb21 100644
--- a/src/emacs/lean-type.el
+++ b/src/emacs/lean-type.el
@@ -33,13 +33,16 @@
   (interactive)
   (lean-get-info-record-at-point 'lean-fill-placeholder-cont))
 
-(defun lean-eldoc-documentation-function-cont (info-record)
+(defun lean-eldoc-documentation-function-cont (info-record &optional add-to-kill-ring)
   "Continuation for lean-eldoc-documentation-function"
   (let ((info-string (lean-info-record-to-string info-record)))
     (when info-string
+      (when add-to-kill-ring
+        (kill-new
+         (substring-no-properties info-string)))
       (message "%s" info-string))))
 
-(defun lean-eldoc-documentation-function ()
+(defun lean-eldoc-documentation-function (&optional add-to-kill-ring)
   "Show information of lean expression at point if any"
   (interactive)
   (cond ((and lean-flycheck-use
@@ -50,7 +53,14 @@
                   (not (eolp)))
              (and (looking-back (rx (not white)))
                   (not (bolp))))
-         (lean-get-info-record-at-point 'lean-eldoc-documentation-function-cont))))
+         (lean-get-info-record-at-point
+          (lambda (info-record)
+            (lean-eldoc-documentation-function-cont info-record add-to-kill-ring))))))
+
+(defun lean-show-type ()
+  "Show information of lean-expression at point if any."
+  (interactive)
+  (lean-eldoc-documentation-function lean-show-type-add-to-kill-ring))
 
 ;; =======================================================
 ;; eval