 (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-type-parse (seq)
  (when (lean-info-type-p seq)
    (let ((header (lean-info-type-parse-header (car seq)))
        (body (cdr seq)))
    `(TYPE ,header ,body))))
(defun lean-info-type-body (typeinfo)
  (cl-third typeinfo))
(defun lean-info-type-body-str (typeinfo)

           (body (-split-on  "--" (cdr seq)))
           (coerced-expr (cl-first body))
           (coerced-type (cl-second body)))
      `(COERCION ,header ,coerced-expr ,coerced-type))))
(defun lean-info-coercion-expr (coercion)
  (cl-third coercion))
(defun lean-info-coercion-expr-str (coercion)
