 (def ^:private +examples-enabled+)
 
 (def +reserved-symbols+
-  '#{kind type □ * ∗ ✳ lambda λ prod forall ∀})
+  '#{kind type □ * ∗ ✳ lambda λ prod forall ∀ _arrow})
 
 (defn reserved-symbol? [s]
   (or (contains? +reserved-symbols+ s)

    (cond
      (lambda-kw? (first t)) (parse-lambda-term def-env t bound)
      (product-kw? (first t)) (parse-product-term def-env t bound)
      (contains? def-env (first t)) (parse-defined-term def-env t bound)
      :else (parse-application-term def-env t bound))))


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

(defn parse-terms [def-env ts bound]
  (reduce (fn [res t]
