 ;; is found).
 ;;}
 
-(comment
-
-  ;; example of a definition with autoimplicit type arguments
-
-  (definition ex
-    "existential"
-    [[P (==> ?T :type)]]
-    (forall [α :type]
-            (==> (forall [x T] (==> (P x) α))
-                 α)))
-
-  ;; should produce (1) the following definiion
-
-  (definition ex-def
-    "explicit version of [[ex]]"
-    [[T :type] [P (==> T :type)]]
-    (forall [α :type]
-            (==> (forall [x T] (==> (P x) α))
-                 α)))
-
-  ;; this is obtained from the following structure
-  '[[?T]]
-  
-  ;; and (2) the following implicit
-  
-  (defimplicit ex
-    "existential" ;; same doc as what would create the definition
-    [def-env ctx [P-term P-type]]
-    (let [[T _] (decompose-impl-type P-ty)]
-      (#'ex-def T P-ty)))
-
-  ;; this is obtained from the following structure
-  '[[P ['==> T _]]]
-
-  ;; and the generation environment
-  {'==> decompose-impl-type}
-) 
-
 (defn ^:no-doc gen-type-parameters-defimplicit
   "Generate the defimplicit for definitions with implicit type parameters."
-  [def-name doc explicit-def-name implicit-types new-params body]
+  [def-name def-kind doc explicit-def-name implicit-types real-params explicit-params body]
   (let [def-env-var (gensym "def-env")
         ctx-var (gensym "ctx")
-        ndoc (mk-def-doc "Definition" body (str doc "\n see [[" explicit-def-name "]]"))
+        ndoc (mk-def-doc def-kind body (str doc "\nsee [[" explicit-def-name "]]"))
         [targs defparams] (reduce (fn [[targs defparams] [param param-ty]]
                                     (if (contains? implicit-types param)
                                       [targs defparams]
                                       (let [param-ty-var (gensym (str param "-ty"))]
                                         [(conj targs [param-ty-var param-ty])
                                          (conj defparams [(gensym (str param "-term")) param-ty-var])])))
-                                  [[] []] new-params)
-        _ (println "targs=" targs)
-        _ (println "defparams=" defparams)
+                                  [[] []] explicit-params)
         [remaining-implicit-types lt-clauses] 
         (reduce (fn [[itypes lt-clauses] param]
-                  (println "==== param = " param)
-                  (println "itypes=" itypes)
-                  (println "lt-clauses=" lt-clauses)
                   (let [[itypes' lt-clause] 
-                        (u/fetch-implicit-type-parameter-handler itypes def-env-var ctx-var param)
-                        _ (println "itypes'=" itypes')
-                        _ (println "lt-cause=" lt-clause)]
+                        (u/fetch-implicit-type-parameter-handler itypes def-env-var ctx-var param)]
                     [itypes' (if (nil? lt-clause)
                                lt-clauses
                                (conj lt-clauses lt-clause))])) [implicit-types []] targs)]

            {def-env :def-env ctx :ctx params :params} header]
        (when (defenv/registered-definition? def-name)
          (println "[Warning] redefinition as implicit"))
        (let [metadata (merge (meta &form) {:doc (mk-impl-doc def-name (mapv #(if (vector? %)
                                                                                (first %)
                                                                                %) params) doc)})]
          `(do
             (def ~def-name (defenv/->Implicit '~def-name (fn [~def-env ~ctx ~@params] ~@body)))
             (alter-meta! (var ~def-name) #(merge % (quote ~metadata)))


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