LaTTe Template

(ns latte-hello-world
  (:refer-clojure :exclude [and or not set =])
  (:require [latte.core
             :as latte
             :refer [defthm defimplicit definition example defaxiom
                     proof assume have pose qed
                     type-check?]]
            [latte-prelude.fun :refer [injective surjective compose]]
            [latte-sets.core :refer [set elem set-equal emptyset] :as sets]
            [latte-prelude.equal :as e]
            [latte-prelude.prop :refer [not and or absurd]]
            [latte-prelude.quant :refer [exists ex ex-elim] :as q]
            [latte-sets.core :as sets]))

(defthm hello-thm 
  "From A and A->B follows B"
  [[A :type][B :type]]
  (==> A (==> A B) B))

(proof 'hello-thm
  (assume [a A, f (==> A B)]
    (have a->b B :by (f a)))
  (qed a->b))