diff --git a/racket-extended-for-implementing-typed-langs.rkt b/racket-extended-for-implementing-typed-langs.rkt
index dc283ec..b3c32c5 100644
--- a/racket-extended-for-implementing-typed-langs.rkt
+++ b/racket-extended-for-implementing-typed-langs.rkt
@@ -1,17 +1,21 @@
-#lang racket/base
+#lang racket
 (require 
+  racket/stxparam
   (for-syntax 
-   racket/base syntax/parse syntax/parse/experimental/template 
-   racket/syntax syntax/stx
+   ;racket/base 
+   syntax/parse syntax/parse/experimental/template 
+   racket/syntax syntax/stx;racket/stxparam syntax/id-table
    "stx-utils.rkt")
   (for-meta 2 racket/base syntax/parse))
 (require "typecheck.rkt")
-(provide (except-out (all-from-out racket/base) #%module-begin))
+(provide (except-out (all-from-out racket) #%module-begin))
 
 ;; Extension of Racket for implementing typed languages
 
-(provide define-simple-syntax/type-rule
+(provide define-typed-syntax ;define-typed-top-level-syntax
+         define-primop ;define-syntax/type-rule
          declare-base-type declare-base-types)
+         ;$this (for-syntax extends))
 (provide (rename-out [mb/ext #%module-begin]))
 ;; provide syntax-classes
 (provide (for-syntax integer str boolean))
@@ -26,47 +30,103 @@
 (define-syntax-rule (declare-base-types τ ...)
   (begin (declare-base-type τ) ...))
 
+;(begin-for-syntax
+;  (define defined-names (make-free-id-table)))
+;(define-syntax-parameter
+;  $this 
+;  (λ (stx) 
+;    (syntax-parse stx
+;      [(_ x) 
+;       #:when (printf "~a\n" (free-id-table-ref defined-names #'λ))
+;       (free-id-table-ref defined-names #'x)])))
+
 (begin-for-syntax
   ;; concrete-τ? : determines if a type is a concrete type or has pattern vars
   ;; result is used to determine whether to insert ellipses in the output pattern
   (define (concrete-τ? τ)
     (or (and (identifier? τ) (member τ lit-set free-identifier=?))
         (and (not (identifier? τ)) (stx-andmap concrete-τ? τ))))
+  ;; ** syntax-class: type ----------------------------------------
   (define-syntax-class type
     (pattern any))
-  ;; meta-term is the term pattern in meta-language
+  ;; **syntax-class: meta-term ----------------------------------------
+  ;; - is the term pattern in meta-language
   ;; (ie where the type rules are declared)
   ;; - matches type vars
   (define-syntax-class meta-term #:datum-literals (:)
+    ;; define-like binding form
+    (pattern (name:id (f:id [x:id : τ] ... (~optional (~and ldots (~literal ...)))) : τ_result e ...)
+     #:attr args-pat/notypes (template ((f x ... (?? ldots)) e ...))
+     #:attr typevars-pat (template (τ_result τ ... (?? ldots))))
+    ;; lambda-like binding form
     (pattern (name:id ([x:id : τ] ... (~optional (~and ldots (~literal ...)))) e ...)
-     #:attr args/notypes (template ((x ... (?? ldots)) e ...))
-     #:attr typevars (template (τ ... (?? ldots))))
+     #:attr args-pat/notypes (template ((x ... (?? ldots)) e ...))
+     #:attr typevars-pat (template (τ ... (?? ldots))))
+    ;; let-like binding form
+    (pattern (name:id ([x:id ex] ... (~optional (~and ldots (~literal ...)))) e ...)
+     #:attr args-pat/notypes (template (([x ex] ... (?? ldots)) e ...))
+     #:attr typevars-pat #'())
+    ;; the list of ids after the name is in curly parens and represents a type declaration
+    ;; for the arguments (which can be any type)
+    ;; example: cons
+    (pattern (name:id τs e ...)
+     #:when (curly-parens? #'τs)
+     #:attr args-pat/notypes #'(e ...)
+     #:attr typevars-pat #'τs)
     (pattern (name:id e ...)
-     #:attr args/notypes #'(e ...)
-     #:attr typevars #'())
-    #;(pattern (name:id . n)
-     #:attr args/notypes #'n
-     #:attr typevars #'()))
-  ;; term matches concrete terms in the actual (typed) language
+     #:attr args-pat/notypes #'(e ...)
+     #:attr typevars-pat #'()))
+  ;; **syntax-class: term ----------------------------------------
+  ;; - matches concrete terms in the actual (typed) language
   ;; - matches concrete types
   ;; name identifier is the extended form
-  (define-syntax-class term
+  (define-syntax-class term #:datum-literals (:)
+    ;; define-like binding form
+    (pattern (name:id (f:id [x:id : τ] ...) : τ_result e ...)
+;     #:with (lam xs+ . es+) (with-extended-type-env #'([x τ] ...)
+;                                   (expand/df #'(λ (f x ...) e ...)))
+;     ;; identifiers didnt get a type bc racket has no %#var form
+;     #:with es++ (with-extended-type-env #'([x τ] ...)
+;                  (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
+;     #:attr expanded-args #'(xs+ . es++)
+     #:attr expanded-args #'((f x ...) e ...)
+     #:attr types #'(τ_result τ ...))
+    ;; lambda-like binding form
     (pattern (name:id ([x:id : τ] ...) e ...)
      #:with (lam xs+ . es+) (with-extended-type-env #'([x τ] ...)
+                              (expand/df #'(λ (x ...) e ...)))
+     ;; identifiers didnt get a type bc racket has no %#var form
+     #:with es++ (with-extended-type-env #'([x τ] ...)
+                   (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
+     #:attr expanded-args #'(xs+ . es++)
+     #:attr types #'(τ ...))
+    ;;let-like binding form
+    (pattern (name:id ([x:id ex] ...) e ...)
+     #:with (ex+ ...) (stx-map expand/df #'(ex ...))
+     #:with (τ ...) (stx-map typeof #'(ex+ ...))
+     #:with (lam (x+ ...) . es+) (with-extended-type-env #'([x τ] ...)
                                    (expand/df #'(λ (x ...) e ...)))
      ;; identifiers didnt get a type bc racket has no %#var form
      #:with es++ (with-extended-type-env #'([x τ] ...)
                   (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
-     #:attr expanded-args #'(xs+ . es++)
-     #:attr types #'(τ ...))
+     #:attr expanded-args #'(([x+ ex+] ...) . es++)
+     #:attr types #'())
+    ;; the list of ids after the name is in curly parens and represents a type declaration
+    ;; for the arguments (which can be any type)
+    ;; example: cons
+    (pattern (name:id τs e ...)
+     #:when (curly-parens? #'τs)
+     #:with (e+ ...) (stx-map expand/df #'(e ...))
+     #:attr expanded-args #'(e+ ...)
+     #:attr types #'τs)
     (pattern (name:id e ...)
      #:with (e+ ...) (stx-map expand/df #'(e ...))
      #:attr expanded-args #'(e+ ...)
-     #:attr types #'())
-    #;(pattern (name:id . n)
-     #:attr expanded-args #'n
      #:attr types #'()))
-  (define-splicing-syntax-class τ-constraint #:datum-literals (:= : let typeof ==)
+  ;; **syntax-class: τ-constraint ----------------------------------------
+  (define-splicing-syntax-class 
+    τ-constraint 
+    #:datum-literals (:= : let typeof == Γ-extend)
     (pattern (let τ := (typeof e))
      #:attr pattern-directive #'(#:with τ (typeof #'e)))
     (pattern (e : τ)
@@ -75,6 +135,9 @@
      #:attr pattern-directive #'(#:fail-unless (type=? #'τ1 #'τ2)
                                                (format "type ~a and ~a should be equal"
                                                        (syntax->datum #'τ1) (syntax->datum #'τ2))))
+    (pattern (Γ-extend [f : τ] ... (~optional (~and ldots (~literal ...))))
+     #:attr pattern-directive
+            #`(#:when (Γ (type-env-extend #'([f τ] ... #,@(template ((?? ldots))))))))
     (pattern (~seq (e0 : τ0) (~literal ...))
      #:when (concrete-τ? #'τ0)
      #:attr pattern-directive #'(#:when (stx-andmap (λ (e) (assert-type e #'τ0)) #'(e0 (... ...)))))
@@ -83,14 +146,15 @@
      #:attr pattern-directive #'(#:when (stx-andmap assert-type #'(e0 (... ...)) #'(τ0 (... ...)))))))
 
           
-
-;; define-term/type-rule
-(define-syntax (define-simple-syntax/type-rule stx)
+;; define-typed-syntax
+(define-syntax (define-typed-syntax stx)
   (syntax-parse stx #:datum-literals (:)
     [(_ meta-e:meta-term : meta-τ
         (~optional (~seq #:where
-                         c:τ-constraint ...)))
+                         c:τ-constraint ...))
+        (~optional (~seq #:expanded expanded-e)))
      #:with fresh-name (generate-temporary #'meta-e.name)
+;     #:when (free-id-table-set! defined-names #'meta-e.name #'fresh-name)
      #:with lits lit-set
      (template
       (begin
@@ -100,24 +164,41 @@
             [e:term
              ;; shadow pattern vars representing subterms with its expansion
              ;; - except for the name of the form, since result must use base form
-             #:with meta-e.args/notypes #'e.expanded-args
-             #:with meta-e.typevars #'e.types
+             #:with meta-e.args-pat/notypes #'e.expanded-args
+             #:with meta-e.typevars-pat #'e.types
              (?? (?@ . ((?@ . c.pattern-directive) ...)))
-             (⊢ (syntax/loc stx (meta-e.name . meta-e.args/notypes)) #'meta-τ)]
+             (⊢ (syntax/loc 
+                  stx 
+                  (?? expanded-e
+                      (meta-e.name . meta-e.args-pat/notypes)))
+                #'meta-τ)]
             [_ #:when (type-error #:src stx #:msg "type error") #'(void)]
             ))))]))
-             
-;; overload mod-begin to check for define-literal-type-rule
+
+
+;; overload mod-begin to check for define-literal-type-rule and other top-level forms
 (begin-for-syntax
-  (define-syntax-class def #:datum-literals (define-literal-type-rule extends)
-    (pattern (extends m ...)
-     #:attr other #'() #:attr stxc #'() #:attr lit-τ #'()
-     #:attr base-mod #'(m ...))
+  (define-syntax-class def #:datum-literals (define-literal-type-rule extends inherit-types)
+    (pattern (extends m f ...)
+;     #:when (stx-map 
+;             (λ (f) 
+;               (free-id-table-set! 
+;                defined-names 
+;                f 
+;                (format-id #'m "ext:~a" f)))
+;             #'(f ...))
+     #:attr other #'() #:attr stxc #'() #:attr lit-τ #'() #:attr inherited-τs #'()
+     #:attr base-mod #'(m) #:attr ext-fs #'(f ...))
+    (pattern (inherit-types τ ...)
+     #:attr inherited-τs #'(τ ...)
+     #:attr other #'() #:attr stxc #'() #:attr lit-τ #'() #:attr base-mod #'() #:attr ext-fs #'())
     (pattern (define-literal-type-rule stx-class : τ)
-     #:attr other #'() #:attr base-mod #'()
+     #:attr other #'() #:attr base-mod #'() #:attr ext-fs #'() #:attr inherited-τs #'()
      #:attr stxc #'(stx-class)
      #:attr lit-τ #'(τ))
-    (pattern any #:attr other #'(any) #:attr stxc #'() #:attr lit-τ #'() #:attr base-mod #'())))
+    (pattern any 
+     #:attr other #'(any) 
+     #:attr stxc #'() #:attr lit-τ #'() #:attr base-mod #'() #:attr ext-fs #'() #:attr inherited-τs #'())))
 
 (define-syntax (mb/ext stx)
   (syntax-parse stx
@@ -125,6 +206,8 @@
      #:with (stxc ...) (template ((?@ . d.stxc) ...))
      #:with (lit-τ ...) (template ((?@ . d.lit-τ) ...))
      #:with (base-mod ...) (template ((?@ . d.base-mod) ...))
+     #:with (inherited-τ ...) (template ((?@ . d.inherited-τs) ...))
+     #:when (set! lit-set (append (syntax->list #'(inherited-τ ...)) lit-set))
      ;; check that 
      #:fail-unless (let ([len (stx-length #'(base-mod ...))]) (or (zero? len) (= len 1)))
                    (format "Supply either 0 or 1 base modules. Given ~a"
@@ -132,48 +215,65 @@
      #:with m (if (zero? (stx-length #'(base-mod ...)))
                   #'()
                   (car (syntax->list #'(base-mod ...))))
+     #:with (f ...) (template ((?@ . d.ext-fs) ...))
+     #:with (ext-f ...) (stx-map (λ (f) (format-id #'m "ext:~a" f)) #'(f ...))
+;                                 (template ((?@ . d.ext-fs) ...)))
      #:with my-datum (generate-temporary)
      #:with datum-def
             #`(define-syntax (my-datum stx)
                 (syntax-parse stx
                   [(_ . x) #:declare x stxc (⊢ (syntax/loc stx (r:#%datum . x)) #'lit-τ)]
                   ...
+                  ;; try previous version of #%datum, if it exists, ie if we are extending
                   #,@(if (stx-null? #'m)
-                  #'()
-                  #`([(_ . x) 
-;                   ;; prev-datum = #%datum in the meta-language
-;                   #:with prev-datum (datum->syntax stx '#%datum)
-;                   #:with racket-datum (datum->syntax stx 'r:#%datum)
-;                   ; when prev-datum is not racket's #%datum
-;                   #:when (not (free-identifier=? #'prev-datum #'racket-datum))
-                   (syntax/loc stx (#,(datum->syntax stx 'ext:#%datum) . x))]))
+                         #'()
+                         #`([(_ . x) 
+                             (syntax/loc stx (#,(datum->syntax #'m 'ext:#%datum) . x))]))
                   [(_ . x) 
                    #:when (type-error #:src stx #:msg "Don't know the type for literal: ~a" #'x)
                    (syntax/loc stx (r:#%datum . x))]))
-            #`(#%module-begin
+     #:with my-mb (generate-temporary)
+     #:with mb-def
+            #'(define-syntax (my-mb stx)
+                (syntax-parse stx
+                  [(_ def (... ...))
+                   #:with mb-let (expand/df #'(r:let () def (... ...) (r:void)))
+                   #'(r:#%module-begin mb-let)]))
+     #`(#%module-begin
+;        (require (for-syntax syntax/id-table))
+;        (begin-for-syntax
+;          (define defined-names (make-free-id-table)))
         #,@(if (stx-null? #'m)
                #'()
-               #`((require (prefix-in ext: m))
+               #`((require (only-in m inherited-τ ...))
+                  (provide inherited-τ ...)
                   (require racket/provide)
+                  (require (prefix-in ext: (except-in m inherited-τ ...)))
                   (provide 
                    (filtered-out
                     (lambda (name)
+                      #;(printf "inheriting from ~a: ~a\n"
+                                #,(syntax->datum #'m)
+                                (and (regexp-match? #rx"^ext:.+$" name)
+                                     (regexp-replace #rx"ext:" name "")))
                       (and (regexp-match? #rx"^ext:.+$" name)
                            (regexp-replace #rx"ext:" name "")))
                     (except-out (all-from-out m) 
-                                #,(datum->syntax stx 'ext:#%datum) 
-                                #,(datum->syntax stx 'ext:check-type-error)
-                                #,(datum->syntax stx 'ext:check-type)
-                                #,(datum->syntax stx 'ext:check-not-type)
-                                #,(datum->syntax stx 'ext:check-type-and-result)))
-                    )))
+                                ext-f ...
+                                #,(datum->syntax #'m 'ext:#%datum) 
+                                #,(datum->syntax #'m 'ext:#%module-begin)
+                                #,(datum->syntax #'m 'ext:check-type-error)
+                                #,(datum->syntax #'m 'ext:check-type)
+                                #,(datum->syntax #'m 'ext:check-not-type)
+                                #,(datum->syntax #'m 'ext:check-type-and-result))))))
         (require (prefix-in r: racket/base))
-        (provide (rename-out [r:#%module-begin #%module-begin]
-                             [r:#%top-interaction #%top-interaction]))
+        (provide (rename-out [r:#%top-interaction #%top-interaction]))
         (provide (rename-out [my-datum #%datum]))
         datum-def
+        (provide (rename-out [my-mb #%module-begin]))
+        mb-def
         #,@(template ((?@ . d.other) ...))
-        ;; testing forms
+        ;; testing forms --------------------
         (require (for-syntax rackunit))
         (require rackunit)
         (provide check-equal?)
diff --git a/stlc+define+cons-via-racket-extended-tests.rkt b/stlc+define+cons-via-racket-extended-tests.rkt
index af2c612..e1a3087 100644
--- a/stlc+define+cons-via-racket-extended-tests.rkt
+++ b/stlc+define+cons-via-racket-extended-tests.rkt
@@ -7,73 +7,74 @@
 
 ;; 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-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))
-;
+(check-type (λ ([x : Int]) (void) x) : (Int → Int))
+(check-type-error (λ ([x : Int]) 1 x))
+(check-type (λ ([x : Int]) (void) (void) x) : (Int → Int))
+
+; printf
 ;(check-type (λ ([x : Int]) (printf {Int} "~a\n" x) x) : (Int → Int))
 ;(check-type-error (λ ([x : Int]) (printf {String} "~a\n" x) x))
 ;(check-type-error (λ ([x : Int]) (printf {Int} 1 x) x))
 ;(check-type (λ ([x : Int]) (printf "one") x) : (Int → Int))
 ;(check-type-error (λ ([x : Int]) (printf "~a" x) x))
 ;(check-type-and-result ((λ ([x : Int]) (printf {Int} "~a\n" x) (+ x 1)) 100) : Int => 101)
-;
-;;; multi arity primops
-;(check-type (λ ([x : Int]) (- 1)) : (Int → Int))
-;(check-type (λ ([x : Int]) (- x x)) : (Int → Int))
-;(check-type (λ ([x : Int]) (- x x x 1)) : (Int → Int))
-;(check-type (λ ([x : Int]) (- x x x x 1)) : (Int → Int))
-;(check-type-and-result ((λ ([x : Int]) (- x x 1)) 10) : Int => -1)
-;(check-type-and-result ((λ ([x : Int]) (- x)) 10) : Int => -10)
-;(check-type-error (λ ([y : Int] [z : Int]) (= y)))
-;(check-type (λ ([y : Int] [z : Int]) (= y z)) : (Int Int → Bool))
-;(check-type (λ ([y : Int] [z : Int]) (= y z z)) : (Int Int → Bool))
-;(check-type-error (λ ([y : Int] [z : Int]) (< y)))
-;(check-type (λ ([y : Int] [z : Int]) (< y z)) : (Int Int → Bool))
-;(check-type (λ ([y : Int] [z : Int]) (< y z z)) : (Int Int → Bool))
-;(check-type (λ ([f : (Int → Int)] [x : Int]) (f x)) : ((Int → Int) Int → Int))
-;;; the following still fails bc varargs not handled
-;;(check-type ((λ ([f : (Int Int → Int)] [x : Int]) (f x x)) + 1) : Int)
-;(check-type-and-result ((λ ([f : (Bool → Bool)] [b : Bool]) (f b)) not #f) : Bool => #t)
-;(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs 1) : Int => 1)
-;(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs (- 1)) : Int => 1)
-;
+
+;; multi arity primops
+(check-type (λ ([x : Int]) (- 1)) : (Int → Int))
+(check-type (λ ([x : Int]) (- x x)) : (Int → Int))
+(check-type (λ ([x : Int]) (- x x x 1)) : (Int → Int))
+(check-type (λ ([x : Int]) (- x x x x 1)) : (Int → Int))
+(check-type-and-result ((λ ([x : Int]) (- x x 1)) 10) : Int => -1)
+(check-type-and-result ((λ ([x : Int]) (- x)) 10) : Int => -10)
+(check-type-error (λ ([y : Int] [z : Int]) (= y)))
+(check-type (λ ([y : Int] [z : Int]) (= y z)) : (Int Int → Bool))
+(check-type (λ ([y : Int] [z : Int]) (= y z z)) : (Int Int → Bool))
+(check-type-error (λ ([y : Int] [z : Int]) (< y)))
+(check-type (λ ([y : Int] [z : Int]) (< y z)) : (Int Int → Bool))
+(check-type (λ ([y : Int] [z : Int]) (< y z z)) : (Int Int → Bool))
+(check-type (λ ([f : (Int → Int)] [x : Int]) (f x)) : ((Int → Int) Int → Int))
+;; the following HO example still fails bc varargs not handled
+;(check-type ((λ ([f : (Int Int → Int)] [x : Int]) (f x x)) + 1) : Int)
+(check-type-and-result ((λ ([f : (Bool → Bool)] [b : Bool]) (f b)) not #f) : Bool => #t)
+(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs 1) : Int => 1)
+(check-type-and-result ((λ ([f : (Int → Int)] [n : Int]) (f n)) abs (- 1)) : Int => 1)
+
 ;; 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)
-;
+(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}))))
-;
+(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)
@@ -82,51 +83,51 @@
 (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)
-;
+(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))
+(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))
 (check-type-and-result (if #t 1 2) : Int => 1)
 (check-type-and-result (if #f 1 2) : Int => 2)
 (check-type-error (if #t 1 #f))
 
-;;;; 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)
+;;; 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)
diff --git a/stlc+define+cons-via-racket-extended.rkt b/stlc+define+cons-via-racket-extended.rkt
index bdaf914..638aa3a 100644
--- a/stlc+define+cons-via-racket-extended.rkt
+++ b/stlc+define+cons-via-racket-extended.rkt
@@ -1,5 +1,6 @@
 #lang s-exp "racket-extended-for-implementing-typed-langs.rkt"
-(extends "stlc-via-racket-extended.rkt")
+(extends "stlc-via-racket-extended.rkt" λ)
+(inherit-types Int →)
 
 ;(require "stlc-via-racket-extended.rkt")
 ;(provide Int → + λ #%app #%top-interaction #%module-begin)
@@ -23,7 +24,7 @@
  define-type cases
  (rename-out
   [datum/tc #%datum]
-  [void/tc void] [printf/tc printf]
+  #;[void/tc void] [printf/tc printf]
   [λ/tc λ] [let/tc let]
   ; for #%app, must prefix and re-provide because this file needs to use racket's #%app
   [stlc:#%app #%app] 
@@ -36,7 +37,7 @@
 
 ;; Simply-Typed Lambda Calculus+
 ;; - stlc extended with practical language feature
-;; - implemented in racket/extended lang
+;; - implemented in racket-extended lang
 ;; Features:
 ;; - stlc
 ;; - multi-expr lam bodies
@@ -71,6 +72,13 @@
      #:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)])))
      #'(begin 
          (struct Cons (x ...) #:transparent))]))
+#;(define-syntax/type-rule #:keywords (variant)
+  [(define-type τ (variant (Cons τ_fld ...) ...))
+   #:where
+   (Γ-extend [Cons : (τ_fld ... → τ)] ...)
+   #:expanded
+   (begin (struct Cons (τ_fld ...) #:transparent) ...)])
+    
 #;(define-syntax (cases stx)
   (syntax-parse stx #:literals (→)
     [(_ e [Cons (x ...) body ... body_result] ...)
@@ -101,7 +109,7 @@
     [(_ . b:boolean) (⊢ (syntax/loc stx (#%datum . b)) #'Bool)]
     [(_ . x) #'(stlc:#%datum . x)]))
 
-(define-simple-syntax/type-rule
+(define-typed-syntax
   (begin e ... e_result) : τ_result
   #:where
   (e : Unit) ...
@@ -118,7 +126,7 @@
   (syntax-parse stx
     [(_) (⊢ (syntax/loc stx (void)) #'Unit)]))
 
-(define-simple-syntax/type-rule
+#;(define-simple-syntax/type-rule
   (void) : Unit)
 
 #;(define-syntax (printf/tc stx)
@@ -136,14 +144,15 @@
      #:when (assert-String-type #'str+)
      (⊢ (syntax/loc stx (printf str+)) #'Unit)]))
 
-;(define-primop + : (Int ... → Int))
-;(define-primop - : (Int Int ... → Int))
-;(define-primop = : (Int Int Int ... → Bool))
-;(define-primop < : (Int Int Int ... → Bool))
-;(define-primop or : (Bool ... → Bool))
-;(define-primop and : (Bool ... → Bool))
-;(define-primop not : (Bool → Bool))
-;(define-primop abs : (Int → Int))
+;(define-primop + : Int ... → Int)
+(define-primop - : Int Int ... → Int)
+(define-primop = : Int Int Int ... → Bool)
+(define-primop < : Int Int Int ... → Bool)
+(define-primop or : Bool ... → Bool)
+(define-primop and : Bool ... → Bool)
+(define-primop not : Bool → Bool)
+(define-primop abs : Int → Int)
+(define-primop void : → Unit)
 
 
 #;(define-syntax (λ/tc stx)
@@ -165,6 +174,13 @@
      #:with τ_body (typeof #'e_result++)
      (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(τ ... → τ_body))]))
 
+(define-typed-syntax
+  (λ ([x : τ] ...) e ... e_result) : (τ ... → τ_body)
+  #:where
+  (e : Unit) ...
+  (let τ_body := (typeof e_result)))
+
+
 ;; #%app
 ;; TODO: support varargs
 #;(define-syntax (app/tc stx)
@@ -187,6 +203,12 @@
      #:when (stx-andmap assert-Unit-type #'(e+ ...))
      (⊢ (syntax/loc stx (let ([x+ e_x+] ...) e+ ... e_result+)) (typeof #'e_result+))]))
 
+(define-typed-syntax
+  (let ([x ex] ...) e ... e_result) : τ_result
+  #:where
+  (e : Unit) ...
+  (let τ_result := (typeof e_result)))
+
 #;(define-syntax (if/tc stx)
   (syntax-parse stx
     [(_ e_test e1 e2)
@@ -200,7 +222,7 @@
                             #'e1 (typeof #'e1+)
                             #'e2 (typeof #'e2+)))
      (⊢ (syntax/loc stx (if e_test+ e1+ e2+)) (typeof #'e1+))]))
-(define-simple-syntax/type-rule
+(define-typed-syntax
   (if e_test e1 e2) : τ2
   #:where
   (e_test : Bool)
@@ -209,6 +231,28 @@
   (τ1 == τ2))
 
 ;; lists ----------------------------------------------------------------------
+(define-typed-syntax
+  (cons {τ} e1 e2) : (Listof τ)
+  #:where
+  (e1 : τ) 
+  (e2 : (Listof τ)))
+(define-typed-syntax
+  (null {τ}) : (Listof τ)
+  #:expanded
+  null)
+(define-typed-syntax
+  (null? {τ} e) : Bool
+  #:where
+  (e : (Listof τ)))
+(define-typed-syntax
+  (first {τ} e) : τ
+  #:where
+  (e : (Listof τ)))
+(define-typed-syntax
+  (rest {τ} e) : (Listof τ)
+  #:where
+  (e : (Listof τ)))
+
 #;(define-syntax (cons/tc stx)
   (syntax-parse stx
     [(_ {T} e1 e2)
@@ -251,86 +295,92 @@
      #'(define f (λ/tc ([x : τ] ...) e ...))]
     [(_ x:id e) #'(define x e)]))
 
+(define-typed-syntax
+  (define (f [x : τ] ...) : τ_result e ...) : Unit
+  #:where
+  (Γ-extend [f : (τ ... → τ_result)])
+  #:expanded
+  (define f (ext:λ ([x : τ] ...) e ...)))
 
-#;(begin-for-syntax
-  ;; EXTENSIBILITY NOTE:
-  ;; Originally, define-type was a #:literal instead of a #:datum-literal, but
-  ;; this became a problem when sysf extended define-type (but not modul-begin).
-  ;; Putting define-type in the #:literals list makes it always expect the stlc
-  ;; version of define-type, so it wasnt getting properly parsed in sysf.
-  ;;
-  ;; Similarly, I had to define the define-type pattern below to avoid explicitly
-  ;; mentioning define-type on the rhs, otherwise it would again lock in the stlc
-  ;; version of define-type.
-  (define-syntax-class maybe-def #:datum-literals (define variant define-type)
-    (pattern define-fn
-             #:with (define (f x ...) body ...) #'define-fn
-             #:attr fndef #'(define-fn)
-             #:attr e #'() #:attr tydecl #'())
-    (pattern define-variant-type-decl
-             #:with (define-type TypeName (variant (Cons fieldτ ...) ...)) 
-                    #'define-variant-type-decl
-             #:attr tydecl #'(define-variant-type-decl)
-             #:attr fndef #'() #:attr e #'())
-    (pattern define-type-decl
-             #:with (define-type TypeName:id (Cons:id fieldτ ...) ...)
-                     #'define-type-decl
-             #:attr tydecl #'(define-type-decl)
-             #:attr fndef #'() #:attr e #'())
-    (pattern exp:expr 
-             #:attr tydecl #'() #:attr fndef #'()
-             #:attr e #'(exp)))
-  (define-syntax-class strct #:literals (begin define-values define-syntaxes)
-    (pattern 
-     (begin
-       (define-values (x ...) mk-strct-type-def)
-       (define-syntaxes (y) strct-info-def))
-     #:attr def-val #'(define-values (x ...) mk-strct-type-def)
-     #:attr def-syn #'(define-syntaxes (y) strct-info-def)))
-  (define-syntax-class def-val #:literals (define-values)
-    (pattern (define-values (x ...) vals)
-     #:attr lhs #'(x ...)
-     #:attr rhs #'vals))
-  (define-syntax-class def-syn #:literals (define-syntaxes)
-    (pattern (define-syntaxes (x) stxs)
-     #:attr lhs #'x
-     #:attr rhs #'stxs))
-    )
+;#;(begin-for-syntax
+;  ;; EXTENSIBILITY NOTE:
+;  ;; Originally, define-type was a #:literal instead of a #:datum-literal, but
+;  ;; this became a problem when sysf extended define-type (but not modul-begin).
+;  ;; Putting define-type in the #:literals list makes it always expect the stlc
+;  ;; version of define-type, so it wasnt getting properly parsed in sysf.
+;  ;;
+;  ;; Similarly, I had to define the define-type pattern below to avoid explicitly
+;  ;; mentioning define-type on the rhs, otherwise it would again lock in the stlc
+;  ;; version of define-type.
+;  (define-syntax-class maybe-def #:datum-literals (define variant define-type)
+;    (pattern define-fn
+;             #:with (define (f x ...) body ...) #'define-fn
+;             #:attr fndef #'(define-fn)
+;             #:attr e #'() #:attr tydecl #'())
+;    (pattern define-variant-type-decl
+;             #:with (define-type TypeName (variant (Cons fieldτ ...) ...)) 
+;                    #'define-variant-type-decl
+;             #:attr tydecl #'(define-variant-type-decl)
+;             #:attr fndef #'() #:attr e #'())
+;    (pattern define-type-decl
+;             #:with (define-type TypeName:id (Cons:id fieldτ ...) ...)
+;                     #'define-type-decl
+;             #:attr tydecl #'(define-type-decl)
+;             #:attr fndef #'() #:attr e #'())
+;    (pattern exp:expr 
+;             #:attr tydecl #'() #:attr fndef #'()
+;             #:attr e #'(exp)))
+;  (define-syntax-class strct #:literals (begin define-values define-syntaxes)
+;    (pattern 
+;     (begin
+;       (define-values (x ...) mk-strct-type-def)
+;       (define-syntaxes (y) strct-info-def))
+;     #:attr def-val #'(define-values (x ...) mk-strct-type-def)
+;     #:attr def-syn #'(define-syntaxes (y) strct-info-def)))
+;  (define-syntax-class def-val #:literals (define-values)
+;    (pattern (define-values (x ...) vals)
+;     #:attr lhs #'(x ...)
+;     #:attr rhs #'vals))
+;  (define-syntax-class def-syn #:literals (define-syntaxes)
+;    (pattern (define-syntaxes (x) stxs)
+;     #:attr lhs #'x
+;     #:attr rhs #'stxs))
+;    )
 
-#;(define-syntax (module-begin/tc stx)
-  (syntax-parse stx #:literals (begin)
-    [(_ mb-form:maybe-def ...)
-     ;; handle define-type
-     #:with (deftype ...) (template ((?@ . mb-form.tydecl) ...))
-     #:with ((begin deftype+ ...) ...) (stx-map expand/df/module-ctx #'(deftype ...))
-     #:with (structdef ...) (stx-flatten #'((deftype+ ...) ...))
-     #:with (structdef+:strct ...) (stx-map expand/df/module-ctx #'(structdef ...))
-     #:with (def-val:def-val ...) #'(structdef+.def-val ...)
-     #:with (def-val-lhs ...) #'(def-val.lhs ...)
-     #:with (def-val-rhs ...) #'(def-val.rhs ...)
-     #:with (def-syn:def-syn ...) #'(structdef+.def-syn ...)
-     #:with (def-syn-lhs ...) #'(def-syn.lhs ...)
-     #:with (def-syn-rhs ...) #'(def-syn.rhs ...)
-     ;; handle defines
-     #:with (deffn ...) (template ((?@ . mb-form.fndef) ...))
-     #:with (deffn+:def-val ...) (stx-map expand/df/module-ctx #'(deffn ...))
-     #:with (f ...) #'(deffn+.lhs ...)
-     #:with (v ...) #'(deffn+.rhs ...)
-     #:with (e ...) (template ((?@ . mb-form.e) ...))
-     ;; base type env
-   ;  #:when (Γ (type-env-extend #'((+ (Int Int → Int)))))
-;; NOTE: for struct def, define-values *must* come before define-syntaxes
-;; ow, error: "Just10: unbound identifier; also, no #%top syntax transformer is bound"
-     (quasisyntax/loc stx 
-       (#%module-begin
-        #,(expand/df #'(let-values ([def-val-lhs def-val-rhs] ...)
-                         (let-syntax ([def-syn-lhs def-syn-rhs] ...)
-                           (letrec-values ([f v] ...) e ... (void)))))
-        (define #,(datum->syntax stx 'runtime-env)
-          (for/hash ([x:τ '#,(map (λ (xτ) (cons (car xτ) (syntax->datum (cdr xτ))))
-                                  (hash->list (Γ)))])
-            (values (car x:τ) (cdr x:τ))))
-        ))]))
+;#;(define-syntax (module-begin/tc stx)
+;  (syntax-parse stx #:literals (begin)
+;    [(_ mb-form:maybe-def ...)
+;     ;; handle define-type
+;     #:with (deftype ...) (template ((?@ . mb-form.tydecl) ...))
+;     #:with ((begin deftype+ ...) ...) (stx-map expand/df/module-ctx #'(deftype ...))
+;     #:with (structdef ...) (stx-flatten #'((deftype+ ...) ...))
+;     #:with (structdef+:strct ...) (stx-map expand/df/module-ctx #'(structdef ...))
+;     #:with (def-val:def-val ...) #'(structdef+.def-val ...)
+;     #:with (def-val-lhs ...) #'(def-val.lhs ...)
+;     #:with (def-val-rhs ...) #'(def-val.rhs ...)
+;     #:with (def-syn:def-syn ...) #'(structdef+.def-syn ...)
+;     #:with (def-syn-lhs ...) #'(def-syn.lhs ...)
+;     #:with (def-syn-rhs ...) #'(def-syn.rhs ...)
+;     ;; handle defines
+;     #:with (deffn ...) (template ((?@ . mb-form.fndef) ...))
+;     #:with (deffn+:def-val ...) (stx-map expand/df/module-ctx #'(deffn ...))
+;     #:with (f ...) #'(deffn+.lhs ...)
+;     #:with (v ...) #'(deffn+.rhs ...)
+;     #:with (e ...) (template ((?@ . mb-form.e) ...))
+;     ;; base type env
+;   ;  #:when (Γ (type-env-extend #'((+ (Int Int → Int)))))
+;;; NOTE: for struct def, define-values *must* come before define-syntaxes
+;;; ow, error: "Just10: unbound identifier; also, no #%top syntax transformer is bound"
+;     (quasisyntax/loc stx 
+;       (#%module-begin
+;        #,(expand/df #'(let-values ([def-val-lhs def-val-rhs] ...)
+;                         (let-syntax ([def-syn-lhs def-syn-rhs] ...)
+;                           (letrec-values ([f v] ...) e ... (void)))))
+;        (define #,(datum->syntax stx 'runtime-env)
+;          (for/hash ([x:τ '#,(map (λ (xτ) (cons (car xτ) (syntax->datum (cdr xτ))))
+;                                  (hash->list (Γ)))])
+;            (values (car x:τ) (cdr x:τ))))
+;        ))]))
 
 ;; type checking testing: -----------------------------------------------------
 ;(require rackunit)