TAPL with core.typed

arith.clj

(ns arith.core
  (:require [clojure.core.typed :refer [ann defalias Rec U Val Int]]
            [clojure.core.match :refer [match]]))

(defalias Expr
  (Rec [Expr]
    (U '[(Val :zero)]
       '[(Val :succ) Expr])))

(ann evaluate [Expr -> Int])
(defn evaluate [e]
  (match e
    [:zero]    0
    [:succ t1] (inc (evaluate t1))))

(comment
  (clojure.core.typed/check-ns)
  (evaluate [:zero])
  (evaluate [:succ [:zero]])
  (evaluate [:succ [:succ [:zero]]]))

macroexpansion.clj

(def evaluate
  (fn* ([e]
          (try
            (if (let* [and__3973__auto__ (clojure.core/vector? e)]
                      (if and__3973__auto__
                        (clojure.core/== (clojure.core/count e) 1)
                        and__3973__auto__))
              (try
                (let* [e_0__44791 (clojure.core/nth e 0)]
                      (if (clojure.core/= e_0__44791 :zero)
                        0
                        (if :else (throw clojure.core.match/backtrack) nil)))
                (catch Exception e__3853__auto__
                  (if (clojure.core/identical? e__3853__auto__ clojure.core.match/backtrack)
                    (do (throw clojure.core.match/backtrack))
                    (throw e__3853__auto__))))
              (if :else (throw clojure.core.match/backtrack) nil))
            (catch Exception e__3853__auto__
              (if (clojure.core/identical? e__3853__auto__ clojure.core.match/backtrack)
                (do
                  (try
                    (if (let* [and__3973__auto__ (clojure.core/vector? e)]
                              (if and__3973__auto__
                                (clojure.core/== (clojure.core/count e) 2) and__3973__auto__))
                      (try
                        (let* [e_0__44792 (clojure.core/nth e 0)]
                              (if (clojure.core/= e_0__44792 :succ)
                                (let* [t1 (clojure.core/nth e 1)]
                                      (inc (evaluate t1)))
                                (if :else (throw clojure.core.match/backtrack) nil)))
                        (catch Exception e__3853__auto__
                          (if (clojure.core/identical? e__3853__auto__ clojure.core.match/backtrack)
                            (do (throw clojure.core.match/backtrack))
                            (throw e__3853__auto__))))
                      (if :else (throw clojure.core.match/backtrack) nil))
                    (catch Exception e__3853__auto__
                      (if (clojure.core/identical? e__3853__auto__ clojure.core.match/backtrack)
                        (do (throw (new java.lang.IllegalArgumentException (clojure.core/str "No matching clause: " e))))
                        (throw e__3853__auto__)))))
                (throw e__3853__auto__)))))))