   (string= "-- ENDINFO" str))
 (defun lean-info-pos (info)
   (cl-case (lean-info-type info)
-    (TYPE     (lean-typeinfo-pos info))
-    (OVERLOAD (lean-overload-pos info))
-    (SYNTH    (lean-synth-pos    info))))
+    (TYPE       (lean-typeinfo-pos   info))
+    (OVERLOAD   (lean-overload-pos   info))
+    (SYNTH      (lean-synth-pos      info))
+    (IDENTIFIER (lean-identifier-pos info))
+    (SYMBOL     (lean-symbol-pos      info))
+    (NAY        (error "no position information for NAY"))))
 (defun lean-info-line-number (info)
   (cl-first (lean-info-pos info)))
 (defun lean-info-column (info)

             (lean-synth-parse '("-- SYNTH|121|2" "not (eq zero (succ m'))" "→ decidable (eq zero (succ m'))")))
            '(121 2)))


;; Basic
;; -----

           collect line))

(defun lean-infolist-parse (lines)
  "Parse lines into info-list"
  (let ((string-seq-seq (lean-infolist-filter-seq (lean-infolist-split-lines lines))))
    (cl-loop for string-seq in string-seq-seq
             when string-seq
             collect (cond ((lean-typeinfo-str-seq-p string-seq)
                            (lean-typeinfo-parse string-seq))
                           ((lean-overload-str-seq-p string-seq)
                            (lean-overload-parse string-seq))
                           ((lean-synth-str-seq-p string-seq)
                            (lean-synth-parse string-seq))
                           ((lean-identifier-str-seq-p string-seq)
                            (lean-identifier-parse string-seq))
                           ((lean-symbol-str-seq-p string-seq)
                            (lean-symbol-parse string-seq))
                           ((lean-nay-str-seq-p string-seq)
                            (lean-nay-parse string-seq))))))

;; -- test
(cl-assert
