 (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)))))
+                     (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))))
 

(defun lean-info-overload-parse (seq)
  (when (lean-info-overload-p seq)
    (let ((header (lean-info-overload-parse-header (car seq)))
        (body (-split-on "--" (cdr seq))))
    `(OVERLOAD ,header ,body))))

;; -- Test
(cl-assert (lean-info-overload-p 'OVERLOAD))

                "→ decidable (eq zero (succ m'))")))
            '(121 2)))
(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'))")))
                  '("not (eq zero (succ m'))\n→ decidable (eq zero (succ m'))"
                    "not (eq one (succ m'))\n→ decidable (eq zero (succ m'))"
                    "not (eq two (succ m'))\n→ decidable (eq zero (succ m'))")))
