          (types       (-filter 'lean-info-type-p       info-list))
          (overloads   (-filter 'lean-info-overload-p   info-list))
          (synths      (-filter 'lean-info-synth-p      info-list))
+         (coercions   (-filter 'lean-info-coercion-p   info-list))
          (identifiers (-filter 'lean-info-identifier-p info-list))
-         (symbols     (-filter 'lean-info-symbol-p     info-list))
-         (nay         (-filter 'lean-info-nay-p        info-list)))
+         (symbols     (-filter 'lean-info-symbol-p     info-list)))
     (make-lean-info-record :type       types
                            :overload   overloads
                            :synth      synths
+                           :coercion   coercions
                            :identifier identifiers
                            :symbol     symbols
-                           :nay        nay)))
+                           :nay        (lean-info-nay-p   string)
+                           :stale      (lean-info-stale-p string))))
 
 (defun lean-info-record-to-string (info-record)
   "Given typeinfo, overload, and sym-name, compose string information."
   (let* ((type     (cl-first (lean-info-record-type       info-record)))
          (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)))
-         name-str  type-str  overload-str str)
+         (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))

                      (or (lean-info-type-parse string-seq)
                          (lean-info-overload-parse string-seq)
                          (lean-info-synth-parse string-seq)
                          (lean-info-identifier-parse string-seq)
                          (lean-info-symbol-parse string-seq)
                          (lean-info-nay-parse string-seq)))
             when result
             collect result)))


                    (lean-info-id-symbol-body-str id)))
           (id   (lean-info-id-symbol-body-str id))
           (sym  (lean-info-id-symbol-body-str sym))))
    (when coercion
      (setq coercion-str (lean-info-coercion-body-str coercion)))
    (when type
      (setq type-str (lean-info-type-body-str type)))
    (when (and name-str overload)
