 
 (example
  (parse-terms {} '(x y z) #{'x 'z})
- => '[:ko {:msg "Variable out of scope", :term y}])
+ => '[:ok [x y z]])
+
+(defn parse-arrow-term [def-env t bound]
+  (if (< (count t) 3)
+    [:ko {:msg "Arrow (implies) requires at least 2 arguments"
+          :term t
+          :nb-args (count (rest t))}]
+    (let [[status ts'] (parse-terms def-env (rest t) bound)]
+      (if (= status :ko)
+        [:ko {:msg "Cannot parse arrow." :term t :from ts'}]
+        (loop [ts (rest (reverse ts')), res (last ts')]
+          (if (seq ts)
+            (recur (rest ts) (list 'prod ['_arrow (first ts)] res))
+            res))))))
+
+(example
+ (parse-term {} '(--> :type :type))
+ => '(prod [_arrow :type] :type))
+
+(example
+ (parse-term {} '(--> sigma tau mu))
+ => '(prod [_arrow sigma] (prod [_arrow tau] mu)))
 
 (defn parse-defined-term [def-env t bound]
   (let [def-name (first t)


(example
 (parse-term {} '(lambda [x :type] z))
 => '[:ko {:msg "Wrong body in lambda form",
           :term (lambda [x :type] z),
           :from {:msg "Variable out of scope", :term z}}])


(defn parse-product-term [def-env t bound]
  (parse-binder-term def-env 'prod t bound))

  (contains? #{'lambda 'λ} t))

(defn product-kw? [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)

