   (contains? #{'lambda 'λ} t))
 
 (defn product-kw? [t]
-  (contains? #{'prod 'forall '∀} t))
+  (contains? #{'prod 'pi 'Π 'forall '∀} t))
+
+(defn arrow-kw? [t]
+  (contains? #{'imply '--> '-> '=> '==> '→ '➝ '⟶ '⟹} t))
 
 (declare parse-lambda-term
          parse-product-term
+         parse-arrow-term
          parse-defined-term
          parse-application-term)
 


(defn parse-lambda-term [def-env t bound]
  (parse-binder-term def-env 'lambda t bound))
  
(example
 (parse-term {} '(lambda [x :type] x))
 => '[:ok (lambda [x :type] x)])

      (if (not= (:arity sdef) 0)
        [:ko {:msg "Definition is not a constant (arity>0)" :term sym :def sdef}]
        [:ok (list sym)]))
    ;; free variable
    :else [:ok sym]))

(example
 (parse-term {} 'x #{'x}) => '[:ok x])

(example
 (parse-term {} 'x #{'y}) => '[:ok x])

(example
 (parse-term {'x {:arity 0}} 'x)
