                (and sym (string-prefix-p (lean-info-id-symbol-body-str sym) it)))
               (lean-info-overload-names overload))
              ", ")))
+    (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))))
     (when (and name-str type-str)
       (setq str (format "%s : %s"
                         (propertize name-str 'face 'font-lock-variable-name-face)

         (overload (cl-first (lean-info-record-overload   info-record)))
         (synth    (cl-first (lean-info-record-synth      info-record)))
         (coercion (cl-first (lean-info-record-coercion   info-record)))
         (id       (cl-first (lean-info-record-identifier info-record)))
         (sym      (cl-first (lean-info-record-symbol     info-record)))
         (stale    (lean-info-record-stale                info-record))
         name-str type-str coercion-str overload-str str)
    (setq name-str
          (cond
           (synth (lean-info-synth-body-str synth))

                        str)))
    str))

(defun lean-get-info-record-at-point-cont (info-record cont)
  (cond ((lean-info-record-nay info-record)
         (lean-server-debug "executing continucation for get-info-record-at-point %d: NAY DETECTED"
                            lean-global-nay-retry-counter)
         (setq lean-global-nay-retry-counter (1+ lean-global-nay-retry-counter))
         (if (and (< lean-global-nay-retry-counter
                     lean-global-nay-retry-counter-max)
                  (= (length lean-global-async-task-queue) 1))
             ;; Retry
             (lean-get-info-record-at-point cont)
           ;; Stop
           (setq lean-global-nay-retry-counter 0)))
        (t
         (lean-server-debug "executing continucation for get-info-record-at-point: OK")
         (setq lean-global-nay-retry-counter 0)
         (funcall cont info-record))))

(defun lean-get-begin-paren-pos ()
  (save-excursion
    (forward-char 1)
    (backward-list 1)
    `(,(line-number-at-pos) . ,(current-column))))

(defun lean-get-info-record-at-point (cont)
  "Get info-record at the current point"
  (let* ((file-name     (buffer-file-name))
         (line-number   (line-number-at-pos))
         (column-number (current-column))
         (cur-char      (char-after (point)))
         (cmd           (cond ((char-equal cur-char ?\()
                               (lean-cmd-info line-number column-number))
                              ;; TODO(soonhok): give information on '('
                              ;; ((char-equal cur-char ?\))
                              ;;  (let ((begin-pos (lean-get-begin-paren-pos)))
                              ;;    (lean-cmd-info (car begin-pos) (cdr begin-pos))))
                              (t (lean-cmd-info line-number)))))
    (lean-server-debug "get-info-record-at-point: %S" cmd)
    (lean-server-check-current-file file-name)
    (lean-server-send-cmd-async cmd (lambda (info-record)
                                      (lean-get-info-record-at-point-cont info-record
                                                                          cont)))))

(defun lean-get-full-name-at-point-cont (info-record)
  "Continuation of lean-get-full-name-at-point"
