       (is (= (:type impl-refl) '(Π [⇧ A] A)))
       (is (nil? (:proof impl-refl)))
       ;; metadata
+      (is (= (:name (meta #'impl-refl)) 'impl-refl))
       (is (string? (:doc (meta #'impl-refl))))
       (is (= (:arglists (meta #'impl-refl)) '[[[A :type]]]))
       (is (not (:private (meta #'impl-refl))))))


(deftest simple-axiom
  (testing "a dummy axiom"
    (is (defenv/axiom? dummy-ax))))







(deftest simple-definition
  (testing "disjunction"
    (is (defenv/definition? disjunction))
    (is (= (:name disjunction) 'disjunction))
    (is (= (:params disjunction) '[[A ✳] [B ✳]]))
    (is (= (:arity disjunction) 2))
    (is (= (:parsed-term disjunction) '(Π [C ✳] (Π [⇧ (Π [⇧ A] C)] (Π [⇧ (Π [⇧ B] C)] C)))))
    (is (= (:type disjunction) '✳))
    (is (= (:opts disjunction ){}))
    ;; metadata
    (is (= (:name (meta #'disjunction)) 'disjunction))
    (is (string? (:doc (meta #'disjunction))))
    (is (= (:arglists (meta #'disjunction)) '([[A :type] [B :type]])))
    ))


;;{
;; Testing theorems
