         `(do
            (def ~def-name ~quoted-def#)
            (alter-meta! (var ~def-name)  (fn [m#] (assoc m#
-                                                         :doc (mk-doc (quote ~body) ~doc)
+                                                         :doc (mk-doc "definition" (quote ~body) ~doc)
                                                          :arglists (list (quote ~params)))))
            [:defined :term (quote ~def-name)])))))
 

      `(do
         (def ~def-name ~quoted-def#)
         (alter-meta! (var ~def-name)  (fn [m#] (assoc m#
                                                       :doc (mk-doc (quote ~ty) ~doc)
                                                       :arglists (list (quote ~params)))))
         [:declared :theorem (quote ~def-name)]))))


      (throw (ex-info "Parameters of defterm must be a vector." {:def-name def-name :params params})))
    [def-name doc params body]))

(defn mk-doc [kind content explanation]
  (str "\n"
       (with-out-str
         (pp/pprint content))
       "\n(" kind ")"
       "\n\n"
       explanation))

(defmacro defterm
