                 "not (eq two (succ m'))"
                 "→ decidable (eq zero (succ m'))")))
             '(121 2)))
-
-(cl-assert (equal (lean-overload-names (lean-overload-parse
+(cl-assert (equal (lean-info-overload-names (lean-info-overload-parse
                                         '("-- OVERLOAD|121|2"
                                           "not (eq zero (succ m'))"
                                           "→ decidable (eq zero (succ m'))"

              ("not (eq one (succ m'))" "→ decidable (eq zero (succ m'))")
              ("not (eq two (succ m'))" "→ decidable (eq zero (succ m'))")))))
(cl-assert (equal
            (lean-overload-pos
             (lean-overload-parse
              '("-- OVERLOAD|121|2"
                "not (eq zero (succ m'))"
                "→ decidable (eq zero (succ m'))"


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

;; -- Test
(cl-assert (lean-info-synth-p 'SYNTH))
(cl-assert (lean-info-synth-p "-- SYNTH|121|2"))
(cl-assert (lean-info-synth-p '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
(cl-assert (equal (lean-info-synth-parse-header "-- SYNTH|121|2")
                  '(121 2)))
(cl-assert (equal (lean-info-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))"))
                  '(SYNTH
                    (121 2)
                    ("not (eq zero (succ m'))"
                     "→ decidable (eq zero (succ m'))"))))
(cl-assert (equal
            (lean-info-synth-pos
             (lean-info-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
            '(121 2)))

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

;; -- Test
(cl-assert (lean-info-identifier-p 'IDENTIFIER))
(cl-assert (lean-info-identifier-p "-- IDENTIFIER|121|2"))
(cl-assert (lean-info-identifier-p '("-- IDENTIFIER|121|2" "foo.f")))
(cl-assert (equal (lean-info-identifier-parse-header "-- IDENTIFIER|121|2")
                  '(121 2)))
(cl-assert (equal (lean-info-identifier-parse '("-- IDENTIFIER|121|2" "foo.f"))
                  '(IDENTIFIER
                    (121 2)
                    ("foo.f"))))
(cl-assert (equal
            (lean-info-identifier-pos
             (lean-info-identifier-parse '("-- IDENTIFIER|121|2" "foo.f")))
            '(121 2)))

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

;; -- Test
(cl-assert (lean-info-symbol-p 'SYMBOL))
(cl-assert (lean-info-symbol-p "-- SYMBOL|121|2"))
(cl-assert (lean-info-symbol-p (lean-info-symbol-parse '("-- SYMBOL|121|2" "→"))))
(cl-assert (equal (lean-info-symbol-parse-header "-- SYMBOL|121|2")
                  '(121 2)))
(cl-assert (lean-info-symbol-p '("-- SYMBOL|121|2" "→")))
(cl-assert (equal (lean-info-symbol-parse '("-- SYMBOL|121|2" "→"))
                  '(SYMBOL
                    (121 2)
                    ("→"))))
(cl-assert (equal
            (lean-info-symbol-pos
             (lean-info-symbol-parse '("-- SYMBOL|121|2" "→")))
            '(121 2)))

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

;; NAY Information
;; ----------------
(defun lean-info-nay-type (nay)
  (cl-first nay))
(defun lean-info-nay-p (nay)
  (pcase nay
    (`NAY t)
    ((pred stringp) (string= "-- NAY" nay))
    ((pred listp) (and (lean-info-nay-p (cl-first nay))))))
(defun lean-info-nay-parse (seq)
  (when (lean-info-nay-p seq)
    '(NAY)))

;; -- Test
(cl-assert (lean-info-nay-p "-- NAY"))
(cl-assert (lean-info-nay-p '("-- NAY")))
(cl-assert (equal (lean-info-nay-parse '("-- NAY"))
                  '(NAY)))

;; Basic
;; -----
(defun lean-info-kind (info)
  (cl-first info))
(defun lean-info-ack-str-p (str)
  (string= "-- ACK" str))
(defun lean-info-begininfo-str-p (str)
  (string= "-- BEGININFO" str))
(defun lean-info-endinfo-str-p (str)
  (string= "-- ENDINFO" str))
(defun lean-info-pos (info)
  (cl-case (lean-info-kind info)
    (TYPE       (lean-info-type-pos   info))
    (OVERLOAD   (lean-info-overload-pos   info))
    (SYNTH      (lean-info-synth-pos      info))
    (IDENTIFIER (lean-info-identifier-pos info))
    (SYMBOL     (lean-info-symbol-pos      info))
    (NAY        ())))
(defun lean-info-line-number (info)
  (cl-first (lean-info-pos info)))
