diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
index cccf20d..0bd72aa 100644
--- a/tapl/ext-stlc.rkt
+++ b/tapl/ext-stlc.rkt
@@ -95,10 +95,10 @@
   (syntax-parse stx #:datum-literals (:)
     [(_ e : ascribed-τ)
      #:with (e- τ) (infer+erase #'e)
-     #:fail-unless (type=? #'ascribed-τ #'τ)
+     #:fail-unless (type=? #'τ #'ascribed-τ)
                    (format "~a does not have type ~a\n"
                            (syntax->datum #'e) (syntax->datum #'ascribed-τ))
-     (⊢ #'e- #'τ)]))
+     (⊢ #'e- #'ascribed-τ)]))
 
 (define-syntax (let/tc stx)
   (syntax-parse stx
diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt
index 52af81b..70833c9 100644
--- a/tapl/stlc+var.rkt
+++ b/tapl/stlc+var.rkt
@@ -1,24 +1,85 @@
 #lang racket/base
 (require
-  (for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
+  (for-syntax racket/base syntax/parse syntax/stx racket/syntax racket/string
+              "stx-utils.rkt" "typecheck.rkt")
+  (for-meta 2 racket/base syntax/parse racket/syntax)
   "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ))
-         (except-in "stlc+tup.rkt" #%app λ))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])
-         tup proj)
+(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let))
+         (except-in "stlc+tup.rkt" #%app λ tup proj let))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
 (provide (all-from-out "stlc+tup.rkt"))
- 
+;(provide define-type-alias define-variant module quote submod)
+(provide tup proj var case)
+
+
 ;; Simply-Typed Lambda Calculus, plus variants
+;; define-type-alias (also provided to programmer)
 ;; Types:
 ;; - types from stlc+tup.rkt
+;; - extend tuple type × to include records
+;; - sum type constructor ∨
 ;; Terms:
 ;; - terms from stlc+tup.rkt
+;; - extend tup to include records
+;; - sums (var)
 
-;(provide Integer)
-;(define-syntax Integer (make-rename-transformer #'Int))
-;(define-syntax Integer (λ (stx) (syntax-parse stx [x:id #'Int])))
-(define-type-alias Integer Int)
-;(provide ArithBinOp)
-; expanded form must have context of its use, so it has the proper #%app
-;(define-syntax ArithBinOp (λ (stx) (syntax-parse stx [x:id (datum->syntax #'x '(→ Int Int Int))])))
-(define-type-alias ArithBinOp (→ Int Int Int))
\ No newline at end of file
+(provide define-type-alias)
+(define-syntax (define-type-alias stx)
+  (syntax-parse stx
+    [(_ τ:id τ-expanded)
+     (if (identifier? #'τ-expanded)
+         #'(define-syntax τ (make-rename-transformer #'τ-expanded))
+         #'(define-syntax τ
+             (λ (stx)
+               (syntax-parse stx
+                 ; τ-expanded must have the context of its use, not definition
+                 ; so the appropriate #%app is used
+                 [x:id (datum->syntax #'x 'τ-expanded)]))))]))
+
+;; records
+(define-syntax (tup stx)
+  (syntax-parse stx #:datum-literals (=)
+    [(_ [l:str = e] ...)
+     #:with ((e- τ) ...) (infers+erase #'(e ...))
+     (⊢ #'(list (list l e-) ...) #'(× [l τ] ...))]
+    [(_ e ...)
+     #'(stlc:tup e ...)]))
+(define-syntax (proj stx)
+  (syntax-parse stx
+    [(_ rec l:str)
+     #:with (rec- τ_rec) (infer+erase #'rec)
+     #:fail-unless (×? #'τ_rec) "not record type"
+     #:with (× [l_τ τ] ...) #'τ_rec
+     #:with (l_match τ_match) (str-stx-assoc #'l #'((l_τ τ) ...))
+     (⊢ #'(cadr (assoc l rec)) #'τ_match)]
+    [(_ e ...)
+     #'(stlc:proj e ...)]))
+
+
+(define-type-constructor ∨)
+
+(define-syntax (var stx)
+  (syntax-parse stx #:datum-literals (as =)
+    [(_ l:str = e as τ)
+     #:when (∨? #'τ)
+     #:with (∨ (l_τ τ_l) ...) (eval-τ #'τ)
+     #:with (l_match τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...))
+     #:with (e- τ_e) (infer+erase #'e)
+     #:when (type=? #'τ_match #'τ_e)
+     (⊢ #'(list l e) #'τ)]))
+(define-syntax (case stx)
+  (syntax-parse stx #:datum-literals (of =>)
+    [(_ e [l:str x => e_l] ...)
+     #:with (e- τ_e) (infer+erase #'e)
+     #:when (∨? #'τ_e)
+     #:with (∨ (l_x τ_x) ...) #'τ_e
+     #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
+     #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
+     #:fail-unless (stx-andmap stx-str=? #'(l ...) #'(l_x ...)) "case clauses is not exhaustive"
+     #:with (((x-) e_l- τ_el) ...)
+            (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
+     #:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
+     (⊢ #'(let ([l_e (car e-)])
+            (cond [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...))
+        (stx-car #'(τ_el ...)))]))
+     
\ No newline at end of file
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
index 43cec5c..4764b31 100644
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@@ -16,10 +16,16 @@
 
 (define (stx-member v stx)
   (member v (syntax->list stx) free-identifier=?))
-
+(define (str-stx-member v stx)
+  (member (datum->syntax v) (map datum->syntax (syntax->list stx)) string=?))
+(define (str-stx-assoc v stx)
+  (assoc v (map syntax->list (syntax->list stx)) stx-str=?))
 (define (stx-length stx) (length (syntax->list stx)))
 
 (define (stx-last stx) (last (syntax->list stx)))
 
 (define (stx-list-ref stx i)
-  (list-ref (syntax->list stx) i))
\ No newline at end of file
+  (list-ref (syntax->list stx) i))
+
+(define (stx-str=? s1 s2)
+  (string=? (syntax-e s1) (syntax-e s2)))
\ No newline at end of file
diff --git a/tapl/tests/stlc+var-tests.rkt b/tapl/tests/stlc+var-tests.rkt
index 8b2c561..1ce002b 100644
--- a/tapl/tests/stlc+var-tests.rkt
+++ b/tapl/tests/stlc+var-tests.rkt
@@ -1,12 +1,83 @@
 #lang s-exp "../stlc+var.rkt"
 (require "rackunit-typechecking.rkt")
 
+;; define-type-alias
+(define-type-alias Integer Int)
+(define-type-alias ArithBinOp (→ Int Int Int))
+
 (check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer)
 (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int)
 (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer)
 (check-type + : ArithBinOp)
 (check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
 
+;; records (ie labeled tuples)
+(check-type "Stephen" : String)
+(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+            (× ["name" String] ["phone" Int] ["male?" Bool]))
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+            : String ⇒ "Stephen")
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+            : String ⇒ "Stephen")
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+            : Int ⇒ 781)
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+            : Bool ⇒ #t)
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+                (× ["my-name" String] ["phone" Int] ["male?" Bool]))
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+                (× ["name" String] ["my-phone" Int] ["male?" Bool]))
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+                (× ["name" String] ["phone" Int] ["is-male?" Bool]))
+
+
+(check-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit]))
+(check-not-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
+(typecheck-fail ((λ ([x : (∨ ["coffee" Unit] ["tea" Unit])]) x)
+                 (var "coffee" = (void) as (∨ ["coffee" Unit]))))
+(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
+(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
+            : (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
+
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+   ["coffee" x => 1])) ; not enough clauses
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+   ["coffee" x => 1]
+   ["teaaaaaa" x => 2])) ; wrong clause
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+   ["coffee" x => 1]
+   ["tea" x => 2]
+   ["coke" x => 3])) ; too many clauses
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+   ["coffee" x => "1"]
+   ["tea" x => 2])) ; mismatched branch types
+(check-type
+ (case (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit]))
+   ["coffee" x => x]
+   ["tea" x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool]))
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
+(check-type
+ (case ((λ ([d : Drink]) d)
+        (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool])))
+   ["coffee" x => (+ (+ x x) (+ x x))]
+   ["tea" x => 2]
+   ["coke" y => 3])
+ : Int ⇒ 4)
+
+(check-type
+ (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
+   ["coffee" x => (+ (+ x x) (+ x x))]
+   ["tea" x => 2]
+   ["coke" y => 3])
+ : Int ⇒ 4)
+
+;; previous tests: ------------------------------------------------------------
 ;; tests for tuples -----------------------------------------------------------
 (check-type (tup 1 2 3) : (× Int Int Int))
 (check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index dc437f4..ef20602 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -46,26 +46,13 @@
              [_ #'τ]))
          (define τ (void))
          (define-for-syntax (τ? stx)
-           (syntax-parse stx
+           (syntax-parse (eval-τ stx)
              [(τ_arg (... ...))
               (for/or ([id (syntax->list #'(τ_arg (... ...)))])
                 (type=? #'τ id))]
              [_ #f]))
          )]))
 
-(define-syntax (define-type-alias stx)
-  (syntax-parse stx
-    [(_ τ:id τ-expanded)
-     #`(begin
-         (provide τ)
-         #,(if (identifier? #'τ-expanded)
-               #'(define-syntax τ (make-rename-transformer #'τ-expanded))
-               #'(define-syntax τ
-                   (λ (stx)
-                     (syntax-parse stx
-                       ; τ-expanded must have the context of its use, not definition
-                       ; so the appropriate #%app is used
-                       [x:id (datum->syntax #'x 'τ-expanded)])))))]))
 ;; type classes
 (begin-for-syntax
   (define (errmsg:bad-type τ)
@@ -81,9 +68,10 @@
 
 (begin-for-syntax
   (define (is-type? τ)
-    (if (identifier? τ)
-        (identifier-binding τ)
-        (stx-andmap is-type? τ)))
+    ;(printf "~a\n" τ)
+    (or (string? (syntax-e τ))
+        (and (identifier? τ) (identifier-binding τ))
+        (and (stx-pair? τ) (stx-andmap is-type? τ))))
   ;; ⊢ : Syntax Type -> Syntax
   ;; Attaches type τ to (expanded) expression e.
 ;  (define (⊢ e τ) (syntax-property (quasisyntax/loc e #,e) 'type τ))
@@ -101,6 +89,7 @@
             (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e)))
        (list #'xs+ #'e+ (typeof #'e+))]
       [([x τ] ...) (infer/type-ctxt+erase #'([x : τ] ...) e)]))
+  ; all xs are bound in the same scope
   (define (infers/type-ctxt+erase ctxt es)
     (syntax-parse ctxt
       [(b:typed-binding ...)
@@ -122,7 +111,10 @@
   (define (types=? τs1 τs2)
     (and (= (stx-length τs1) (stx-length τs2))
          (stx-andmap type=? τs1 τs2)))
-  
+  (define (same-types? τs)
+    (define τs-lst (syntax->list τs))
+    (or (null? τs-lst)
+        (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst))))
   ;; typeof : Syntax -> Type or #f
   ;; Retrieves type of given stx, or #f if input has not been assigned a type.
   (define (typeof stx) (syntax-property stx 'type))
@@ -143,16 +135,21 @@
     (stx-andmap assert-type es τs))
 
   (define (eval-τ τ)
-    (define app (datum->syntax τ '#%app)) ; #%app in τ's ctxt
-    ;; stop right before expanding #%app
-    (define maybe-app-τ (local-expand τ 'expression (list app)))
-    ;; manually remove app and recursively expand
-    (if (identifier? maybe-app-τ) ; base type
-        maybe-app-τ
-        (syntax-parse maybe-app-τ
-          [(τ ...)
-           #:with (τ-exp ...) (stx-map eval-τ #'(τ ...))
-           #'(τ-exp ...)])))
+    (syntax-parse τ
+      [s:str τ] ; record field
+      [_
+;       (printf "eval: ~a\n" τ)
+       (define app (datum->syntax τ '#%app)) ; #%app in τ's ctxt
+       ;; stop right before expanding #%app
+       (define maybe-app-τ (local-expand τ 'expression (list app)))
+ ;      (printf "after eval: ~a\n" τ)
+       ;; manually remove app and recursively expand
+       (if (identifier? maybe-app-τ) ; base type
+           maybe-app-τ
+           (syntax-parse maybe-app-τ
+             [(τ ...)
+              #:with (τ-exp ...) (stx-map eval-τ #'(τ ...))
+              #'(τ-exp ...)]))]))
   
   ;; type=? : Type Type -> Boolean
   ;; Indicates whether two types are equal
@@ -168,6 +165,7 @@
       ; adding a type constructor should extend type equality
 ;      #:datum-literals (→)
       [(x:id y:id) (free-identifier=? τ1 τ2)]
+      [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
       [((τ1 ...) (τ2 ...))
        (types=? #'(τ1 ...) #'(τ2 ...))]
       #;[((x ... → x_out) (y ... → y_out))
@@ -244,6 +242,10 @@
                 #:when (stx-andmap assert-type #'es+ #'τs-ext)
                 (⊢ (syntax/loc stx (op . es+)) #'τ_result)])))]))
 
+(define-for-syntax (mk-pred x) (format-id x "~a?" x))
+(define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
+
+       
 ;; type environment -----------------------------------------------------------
 #;(begin-for-syntax