 (defun lean-info-type-parse (seq)
   (when (lean-info-type-p seq)
     (let ((header (lean-info-type-parse-header (car seq)))
-        (body (cdr seq)))
-    `(TYPE ,header ,body))))
+          (body (cdr seq)))
+      `(TYPE ,header ,body))))
 (defun lean-info-type-body (typeinfo)
   (cl-third typeinfo))
 (defun lean-info-type-body-str (typeinfo)

(cl-assert (equal
            (lean-info-coercion-pos
             (lean-info-coercion-parse '("-- COERCION|417|15"
                                              "of_nat")))
            '(417 15)))

;; Identifier Information

(defun lean-get-partial-names (full-name)
  "Given a full-name \"a.b.c.d\", return a set of partial names (\"a.b.c.d\" \"b.c.d\" \"c.d\" \"d\")"
  (cl-labels ((helper(l1 l2 names)
                     (cond (l1 (helper
                                (-butlast l1)
                                (cons nil (-butlast l2))
                                (-zip-with (lambda (x y) (if y (concat x "." y) x))
                                           names
                                           (cons nil (-butlast l2)))))
                           (t (reverse names)))))
    (let ((items (reverse (split-string full-name "\\."))))
      (helper items items items))))

