 ;; https://ncatlab.org/nlab/show/pure+type+system
 
 (defrecord V [name])            (defn v? [x] (instance? V x))
-(defrecord A [vars form])       (defn a? [x] (instance? A x))
+(defrecord A [vars expr args])  (defn a? [x] (instance? A x))
 (defrecord F [vars expr pars])  (defn f? [x] (instance? F x))
 ;; vars : Set V
 ;; pars : Vec V
-;; form : Vec Expr
+;; args : Vec Expr
 
 (defprotocol Expr
   "an expression satisfies the following protocol.

  (fv [this])
  (ev [this dict]))

(defn- fv- [pars expr & exprs]
  (loop [exprs exprs  vars (transient (fv expr))]
    (if-let [[expr & exprs] exprs]
      (recur exprs (reduce conj! vars (fv expr)))
      (persistent! (reduce disj! vars pars)))))

(extend-protocol Expr
  F


(defn ?
  "funcall, the counit of product-exponential adjunction"
  ([expr & args]
   (-> (aa expr args)
       (ev {}))))

(defn %
  "forall"
  ([expr & pars] ; currently pars can only be vars
   (-> (ff expr pars)
       (ev {}))))

(defn !
  "produces a fresh or named var"
