          (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)))
+         (extra    (cl-first (lean-info-record-extra      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)
+         name-str type-str coercion-str extra-str overload-str str)
     (setq name-str
           (cond
            (synth (lean-info-synth-body-str synth))

                                         "of_nat")))
            '(417 15)))

;; Identifier Information
;; ----------------------
(defun lean-info-identifier-type (identifier)

               (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)
