 
   Users (as opposed to developpers) of the framework should
   mostly depend on this namespace."
+
+  (:require [clojure.pprint :as pp])
 
   (:require [latte.utils :as u])
   (:require [latte.presyntax :as stx])

          (let [name# (name def-name)]
            `(do
               (def ~def-name ~quoted-def)
               (alter-meta! (var ~def-name)  (fn [m#] (assoc m# :doc ~doc)))
               [:declared :theorem ~name#])))))))



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