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


  Users (as opposed to developpers) of the framework should
  mostly depend on this namespace."

  (:require [latte.utils :as u])
  (:require [latte.presyntax :as stx])

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

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

(defmacro defterm
  "Defines a mathematical term composed of a `name`, and optional (but highly recommended)
