           (and binding
                (= (second binding) kind)))))
 
+(defn- match-free-var?
+  [expr env]
+  (and (symbol? expr)
+       (not (alist/assoc expr env))))
+
 (defn- match-lambda-var?
   [expr env]
-  (match-bound-var? expr env 'lambda))
+  (match-bound-var? expr env :lambda))
   
 (parser/register-term-other-parser
  match-lambda-var?
  (fn [expr env]
    (mk-lambda-var expr)))
 
-(example (parse 'my-var (list ['my-var 'lambda]))
+(example (parse 'my-var (list ['my-var :lambda]))
          => (mk-lambda-var 'my-var))
 
 (example (parse '(lambda [x (univ 0)] x))
          => (mk-abstraction 'x (mk-univ 0) (mk-lambda-var 'x)))
 
-
 (extend-type LambdaVar
   Unparser
-  (unparse [e] (:name e)))
+  (unparse [e] (:name e))
+  FreeVars
+  (free-vars [e kind] (if (= kind :lambda)
+                        #{(:name e)}
+                        #{})))
 
 (example (unparse (mk-lambda-var 'my-var)) => 'my-var)
 
 (example (unparse (parse '(lambda [x (univ 0)] x)))
          => '(lambda [x (univ 0)] x))
+
+(example (free-vars (:body (parse '(lambda [x (univ 0)] x))) :lambda)
+         => #{'x})
+
+(example (free-vars (:body (parse '(lambda [x (univ 0)] x))) :forall)
+         => #{})
 
 ;;{
 


(extend-type ProductVar
  Unparser
  (unparse [e] (:name e)))

(example (unparse (mk-product-var 'my-var)) => 'my-var)

(example (unparse (parse '(forall [x (univ 0)] x)))
         => '(forall [x (univ 0)] x))

;;}

(ns latte.term
  (:require [clojure.set]
            [latte.utils :refer [example append]]
            [latte.alist :as alist :refer [acons vassoc]]
            [latte.termparser :as parser :refer [parse]]))

