   [:ok :kind])
 
 (example
- (type-of [] :type) => [:ok :kind])
+ (type-of {} [] :type) => [:ok :kind])
 
 ;;{
 ;;        ty::>Type or t::>Kind in E

;;          E |- rator rand : B [rand/x]
;;}

(defn type-of-app [env rator rand]
  (let [[status trator :as res] (type-of env rator)]
    (if (= status :ko)
      res
      (let [trator' (b/normalize trator)]
        (if (not (s/valid? ::sx/product trator'))
          [:ko {:msg "Not a product type" :term rator :type trator :env env}]
          (let [[_ [x A] B] trator']
            (if (not (type-check? env rand A))
              [:ko {:msg "Cannot apply" :dom A :operand rand}]
              [:ok (sx/subst B x rand)])))))))


(example
 (type-of '[[bool :type] [y bool]]
          '((lambda [x bool] x) y)) => '[:ok bool])


(ns latte.typing
  (:require [clj-by.example :refer [example do-for-example]])
  (:require [latte.syntax :as stx])
  (:require [latte.norm :as norm])
  )

(def ^:private +examples-enabled+)
