kencoba

(ns
    ^{:doc
      "Simple Theorem Prover 'Programming Language Theory and its Implementation' Michael J.C. Gordon"
      :author "Kenichi Kobayashi"}
  prover
  (:use [clojure.test])
  (:require [clojure.walk :as cw]))

(def constant #{'+ '- '< '<= '> '>= '* '= 'T 'F 'DIV 'not 'and 'or 'implies})