diff --git a/racket-extended-for-implementing-typed-langs.rkt b/racket-extended-for-implementing-typed-langs.rkt
index 1e8680a..ee79cad 100644
--- a/racket-extended-for-implementing-typed-langs.rkt
+++ b/racket-extended-for-implementing-typed-langs.rkt
@@ -125,7 +125,7 @@
                   ...
                   [(_ . x) 
                    #:when (type-error #:src stx #:msg "Don't know the type for literal: ~a" #'x)
-                   stx]))
+                   (syntax/loc stx (#%datum . x))]))
      (template
       (#%module-begin
        (provide (rename-out [my-datum #%datum]))
diff --git a/stlc-test.rkt b/stlc-test.rkt
deleted file mode 100644
index a8ecf55..0000000
--- a/stlc-test.rkt
+++ /dev/null
@@ -1,5 +0,0 @@
-#lang s-exp "stlc-via-racket-extended.rkt"
-((λ ([f : (Int → Int)] [x : Int]) (f x))
-   (λ ([x : Int]) (+ x x 2))
-   10)
-((λ ([x : Int]) (+ x 1 3)) 100)
\ No newline at end of file
diff --git a/stlc-tests.rkt b/stlc-tests.rkt
index 07fe48d..707eae4 100644
--- a/stlc-tests.rkt
+++ b/stlc-tests.rkt
@@ -1,151 +1,5 @@
-#lang s-exp "stlc+define+cons.rkt"
-
-(check-type-error ((λ ([x : Int]) (+ x 1)) "10"))
-(check-type ((λ ([x : Int]) (+ x 1)) 10) : Int)
-(check-equal? ((λ ([x : Int]) (+ x 1)) 10) 11) ; identifier used out of context
-(check-type-and-result ((λ ([x : Int]) (+ x 1)) 10) : Int => 11)
-
-; check fns with literal or id bodies
-(check-type (λ ([x : Int]) x) : (Int → Int))
-(check-type (λ ([x : Unit] [y : Int]) x y) : (Unit Int → Int))
-
-;; check fns with multi-expr body
-(check-type (λ ([x : Int]) (void) x) : (Int → Int))
-(check-type-error (λ ([x : Int]) 1 x))
-(check-type (λ ([x : Int]) (void) (void) x) : (Int → Int))
-
-; HO fn
-(check-type-and-result ((λ ([f : (Int → Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
-(check-type (λ ([f : (Int → Int)]) (f 10)) : ((Int → Int) → Int))
-(check-type (λ ([f : (Int → Int)]) (λ ([x : Int]) (f (f x)))) : ((Int → Int) → (Int → Int)))
-(check-type-error (λ (f : (Int → Int)) (λ (x : String) (f (f x)))))
-
-;; shadowed var
-(check-type-error ((λ ([x : Int]) ((λ ([x : String]) x) x)) 10))
-(check-type-and-result ((λ ([x : String]) ((λ ([x : Int]) (+ x 1)) 10)) "ten") : Int => 11)
-
-;; let
-(check-type-and-result (let ([x 1] [y 2]) (+ x y)) : Int => 3)
-(check-type-error (let ([x 1] [y "two"]) (+ x y)))
-(check-type-and-result (let ([x "one"]) (let ([x 2]) (+ x x))) : Int => 4)
-
-;; lists
-(check-type-and-result (first {Int} (cons {Int} 1 (null {Int}))) : Int => 1)
-(check-type-and-result (rest {Int} (cons {Int} 1 (null {Int}))) : (Listof Int) => (null {Int}))
-(check-type-error (cons {Int} 1 (null {String})))
-(check-type-error (cons {Int} "one" (null {Int})))
-(check-type-error (cons {String} 1 (null {Int})))
-(check-type-error (cons {String} 1 (null {Int})))
-(check-type-error (cons {String} "one" (cons {Int} "two" (null {String}))))
-(check-type-and-result (first {String} (cons {String} "one" (cons {String} "two" (null {String}))))
-                       : String => "one")
-(check-type-and-result (null? {String} (null {String})) : Bool => #t)
-(check-type-and-result (null? {String} (cons {String} "one" (null {String}))) : Bool => #f)
-(check-type-error (null? {String} (null {Int})))
-(check-type-error (null? {Int} (null {String})))
-(check-type-error (null? {Int} 1))
-(check-type-error (null? {Int} "one"))
-(check-type-error (null? {Int} (cons {String} "one" (null {String}))))
-
-; begin and void
-(check-type (void) : Unit)
-(check-type-and-result (begin (void) 1) : Int => 1)
-(check-type-and-result (begin (void) (void) 1) : Int => 1)
-(check-type-and-result (begin (void) (void) (void)) : Unit => (void))
-(check-type-and-result (begin (+ 1 2)) : Int => 3)
-(check-type-error (begin 1 2))
-
-(check-type (λ ([x : Int]) (void) (+ x 1)) : (Int → Int))
-(check-type-error (λ ([x : Int]) 1 1))
-(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (Int Int → Int))
-(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a (+ b c))) 1 2 3)
-                       : Int => 6)
-
-; define
-(define (g [y : Int]) : Int
-  (+ (f y) 1))
-(define (f [x : Int]) : Int
-  (+ x 1))
-(check-type-and-result (f 10) : Int => 11)
-(check-type-and-result (g 100) : Int => 102)
-(check-not-type (f 10) : String)
-(check-not-type (g 100) : String)
-
-;; if
-(check-type-and-result (if (null? {Int} (null {Int})) 1 2) : Int => 1)
-(check-type-and-result (if (null? {Int} (cons {Int} 1 (null {Int}))) 1 2) : Int => 2)
-(check-type-error (if (null? {Int} (null {Int})) 1 "one"))
-(check-type-error (if (null? {Int} (null {Int})) "one" 1))
-(check-type-error (if 1 2 3))
-
-;;; recursive fn
-(define (add1 [x : Int]) : Int
-  (+ x 1))
-(define (map [f : (Int → Int)] [lst : (Listof Int)]) : (Listof Int)
-  (if (null? {Int} lst)
-      (null {Int})
-      (cons {Int} (f (first {Int} lst)) (map f (rest {Int} lst)))))
-(check-type-and-result (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int})))) 
-                       : (Listof Int)
-                       => (cons {Int} 2 (cons {Int} 3 (null {Int}))))
-(check-not-type (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int})))) 
-                : (Listof String))
-
-;; recursive types
-(define (a [x : Int]) : Int (b x))
-(define (b [x : Int]) : Int (a x))
-(define (ff [x : Int]) : Int (ff x))
-
-;; define-type (non parametric)
-(define-type MaybeInt (variant (None) (Just Int)))
-(check-type (None) : MaybeInt)
-(check-type (Just 10) : MaybeInt)
-(check-type-error (Just "ten"))
-(check-type-error (Just (None)))
-(define (maybeint->bool [maybint : MaybeInt]) : Bool
-  (cases maybint
-   [None () #f]
-   [Just (x) #t]))
-(check-type-and-result (maybeint->bool (None)) : Bool => #f)
-(check-type-and-result (maybeint->bool (Just 25)) : Bool => #t)
-(check-type-error (maybeint->bool 25))
-(check-type-error (define (maybeint->wrong [maybint : MaybeInt])
-                    (cases maybint
-                      [None () #f]
-                      [Just (x) x])))
-
-(define-type IntList (variant (Null) (Cons Int IntList)))
-(check-type-and-result (Null) : IntList => (Null))
-(check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
-(check-type-error (Cons "one" (Null)))
-(check-type-error (Cons 1 2))
-(define (map/IntList [f : (Int → Int)] [lst : IntList]) : IntList
-  (cases lst
-    [Null () (Null)]
-    [Cons (x xs) (Cons (f x) (map/IntList f xs))]))
-(check-type-and-result (map/IntList add1 (Null)) : IntList => (Null))
-(check-type-and-result (map/IntList add1 (Cons 1 (Null))) : IntList => (Cons 2 (Null)))
-(check-type-and-result (map/IntList add1 (Cons 2 (Cons 1 (Null)))) 
-                       : IntList => (Cons 3 (Cons 2 (Null))))
-(check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
-(define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
-(define (map/BoolList [f : (Bool → Int)] [lst : BoolList]) : IntList
-  (cases lst
-    [BoolNull () (Null)]
-    [BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
-(check-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : IntList)
-(check-type-and-result 
- (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolCons #f (BoolNull)))
- : IntList => (Cons 1 (Null)))
-(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
-;; check typename is available
-(check-type (λ ([lst : IntList]) 
-              (cases lst
-                [Null () (None)]
-                [Cons (x xs) (Just x)]))
-            : (IntList → MaybeInt))
-(check-type ((λ ([lst : IntList]) 
-              (cases lst
-                [Null () (None)]
-                [Cons (x xs) (Just x)]))
-             (Null)) : MaybeInt)
\ No newline at end of file
+#lang s-exp "stlc.rkt";"stlc-via-racket-extended.rkt"
+((λ ([f : (Int → Int)] [x : Int]) (f x))
+   (λ ([x : Int]) (+ x x 1))
+   10)
+((λ ([x : Int]) (+ x 1 3)) 100)
\ No newline at end of file
diff --git a/stlc-via-racket-extended.rkt b/stlc-via-racket-extended.rkt
index 2d52f4d..271cd3c 100644
--- a/stlc-via-racket-extended.rkt
+++ b/stlc-via-racket-extended.rkt
@@ -5,7 +5,7 @@
 
 ;; Simply-Typed Lambda Calculus
 ;; - implemented with racket-extended language
-;; - lam, app, and var only
+;; - lam, app, var, +, and int literals only
 
 (declare-built-in-types → Int)
 
diff --git a/stlc.rkt b/stlc.rkt
index 0c42888..f384eab 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -4,14 +4,15 @@
               syntax/stx racket/syntax
               "stx-utils.rkt")
   "typecheck.rkt")
-(provide (rename-out [λ/tc λ] [app/tc #%app] [datum/tc #%datum] [+/tc +]))
+(provide (rename-out [λ/tc λ] [app/tc #%app] [datum/tc #%datum]))
 (provide #%module-begin #%top-interaction)
 
 ;; Simply-Typed Lambda Calculus
-;; - lam, app, and var only
+;; - lam, app, var, +, and int literals only
 ;; - implemented in racket
 
 (define-and-provide-builtin-types → Int)
+(provide (for-syntax assert-Int-type))
 (define-for-syntax (assert-Int-type e) (assert-type e #'Int))
 
 ;; typed forms ----------------------------------------------------------------
@@ -20,17 +21,12 @@
 (define-syntax (datum/tc stx)
   (syntax-parse stx
     [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
-    [(_ x) 
-     #:when (type-error #:src #'x #:msg "~a has unknown type" #'x)
+    [(_ . x) 
+     #:when (type-error #:src #'x #:msg "Literal ~a has unknown type." #'x)
      (syntax/loc stx (#%datum . x))]))
 
 ;; op
-(define-syntax (+/tc stx)
-  (syntax-parse stx 
-    [(_ e ...)
-     #:with es+ (stx-map expand/df #'(e ...))
-     #:when (stx-andmap assert-Int-type #'es+)
-     (⊢ (syntax/loc stx (+ . es+)) #'Int)]))
+(define-primop + : (Int ... → Int))
 
 ;; lambda
 (define-syntax (λ/tc stx)