      ;; When not specified, just return info-list.
      (t info-list))))
 
-(cl-defstruct lean-info-record type overload synth coercion identifier symbol extra nay stale)
+(cl-defstruct lean-info-record type overload synth coercion identifier symbol extra proofstate nay stale)
 
 (defun lean-info-record-parse (string &optional file-name column-number)
   "Parse string into info-record"

                        (format "\n%s with %s"
                                (propertize "overloaded" 'face 'font-lock-keyword-face)
                                overload-str))))
    (when (and stale str)
      (setq str (format "[%s] %s"
                        (propertize "stale" 'face '(foreground-color . "red"))


(defun lean-info-id-symbol-body-str (info)
  (case (lean-info-kind info)
    ('PROOFSTATE (string-join (lean-info-proofstate-body info) "\n"))
    ('IDENTIFIER (string-join (lean-info-symbol-body info) "\n"))
    ('SYMBOL     (string-join (lean-info-identifier-body info) "\n"))))


;; Proofstate Information
;; ----------------
(defun lean-info-proofstate-kind (proofstate)
  (cl-first proofstate))
(defun lean-info-proofstate-p (proofstate)
  (pcase proofstate
    (`PROOFSTATE t)
    ((pred stringp) (string-prefix-p "-- PROOF_STATE" proofstate))
    ((pred listp) (and (lean-info-proofstate-p (cl-first proofstate))))))
(defun lean-info-proofstate-pos (proofstate)
  (cl-second proofstate))
(defun lean-info-proofstate-parse-header (str)
  (let ((items (split-string str "|")))
    (list (string-to-number (cl-second items))
          (string-to-number (cl-third items)))))
(defun lean-info-proofstate-parse (seq)
  (when (lean-info-proofstate-p seq)
    (let ((header (lean-info-proofstate-parse-header (car seq)))
          (body (cdr seq)))
      `(PROOFSTATE ,header ,body))))
(defun lean-info-proofstate-body (proofstate)
  (cl-third proofstate))
(defun lean-info-proofstate-body-str (proofstate)
  (string-join (lean-info-proofstate-body proofstate) "\n"))

;; Basic
;; -----
