 ;; of other `kind` of statements such as theorems or axioms.
 ;;}
 
-(defn ^:no-doc mk-def-doc [kind content explanation]
+(defn ^:no-doc mk-def-doc 
+  [kind content explanation]
   (str "\n```\n"
        (with-out-str
          (pp/pprint content))
        "```\n**" kind "**: "
        (or explanation "")))
-
 
 ;;{
 ;; ## Theorems, lemmas and axioms

                 explicit-def-name (symbol (str def-name "-def"))]
                `(do
                   (definition ~explicit-def-name ~(str "This is an explicit variant of [[" def-name "]].") ~new-params ~body)
                   ~(gen-type-parameters-defimplicit def-name doc explicit-def-name implicit-types new-params body)
                   [:defined :term (quote ~def-name)]
                   ))
            ;; no implicit parmeter types from here...
            (let [[status definition] (handle-term-definition def-name params body)]
          (when (= status :ko)
            (throw (ex-info "Cannot define term." {:name def-name, :error definition})))
          ;;{
          ;;  - Second, after some checks, we register the definition in the currently active namespace (i.e. `*ns*`).
          ;;}          
          (let [quoted-def# definition]
            `(do
               (def ~def-name ~quoted-def#)
               (alter-meta! (var ~def-name)  (fn [m#] (assoc m#
                                                             :doc (mk-def-doc "Definition" (quote ~body) ~doc)
                                                             :arglists (list (quote ~params)))))
               [:defined :term (quote ~def-name)]))))))))

;;{
;; The following function generates a `defimplicit` form that (if successful) synthesizes


(s/def ::iparam any?) ;; (s/tuple symbol? symbol?))

(defn ^:no-doc mk-impl-doc [name explanation]
  ;; XXX: everything in the explanation ?
  explanation)

(defmacro defimplicit
  [& args]
