diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt
index 73f3c67..5f149ea 100644
--- a/turnstile/examples/exist.rkt
+++ b/turnstile/examples/exist.rkt
@@ -16,8 +16,8 @@
 
 (define-typed-syntax pack
   [(pack (τ:type e) as ∃τ:type) ≫
-   [#:with (~∃* (τ_abstract) τ_body) #'∃τ.norm]
-   [#:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body)]
+   #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
+   #:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body)
    [⊢ [e ≫ e- ⇐ : τ_e]]
    --------
    [⊢ [_ ≫ e- ⇒ : ∃τ.norm]]])
@@ -69,7 +69,7 @@
    ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
    ;;
    [⊢ [e_packed ≫ e_packed- ⇒ : (~∃ (Y) τ_body)]]
-   [#:with τ_x (subst #'X #'Y #'τ_body)]
+   #:with τ_x (subst #'X #'Y #'τ_body)
    [([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ [e ≫ e- ⇒ : τ_e]]
    --------
    [⊢ [_ ≫ (let- ([x- e_packed-]) e-) ⇒ : τ_e]]])
diff --git a/turnstile/examples/ext-stlc.rkt b/turnstile/examples/ext-stlc.rkt
index 39d6213..de82559 100644
--- a/turnstile/examples/ext-stlc.rkt
+++ b/turnstile/examples/ext-stlc.rkt
@@ -30,7 +30,7 @@
    --------
    [⊢ [_ ≫ (#%datum- . s) ⇒ : String]]]
   [(#%datum . f) ≫
-   [#:when (flonum? (syntax-e #'f))]
+   #:when (flonum? (syntax-e #'f))
    --------
    [⊢ [_ ≫ (#%datum- . f) ⇒ : Float]]]
   [(#%datum . c:char) ≫
diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt
index eaa5933..02da793 100644
--- a/turnstile/examples/fomega.rkt
+++ b/turnstile/examples/fomega.rkt
@@ -92,7 +92,7 @@
   [(inst e τ ...) ≫
    [⊢ [e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
    [⊢ [τ ≫ τ- ⇐ : k] ...]
-   [#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)]
+   #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
    --------
    [⊢ [_ ≫ e- ⇒ : τ-inst]]])
 
@@ -101,16 +101,16 @@
 (define-typed-syntax tyλ
   [(tyλ bvs:kind-ctx τ_body) ≫
    [() ([bvs.x ≫ tv- : bvs.kind] ...) ⊢ [τ_body ≫ τ_body- ⇒ : k_body]]
-   [#:fail-unless ((current-kind?) #'k_body)
-    (format "not a valid type: ~a\n" (type->str #'τ_body))]
+   #:fail-unless ((current-kind?) #'k_body)
+   (format "not a valid type: ~a\n" (type->str #'τ_body))
    --------
    [⊢ [_ ≫ (λ- (tv- ...) τ_body-) ⇒ : (⇒ bvs.kind ... k_body)]]])
 
 (define-typed-syntax tyapp
   [(tyapp τ_fn τ_arg ...) ≫
    [⊢ [τ_fn ≫ τ_fn- ⇒ : (~⇒ k_in ... k_out)]]
-   [#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
-    (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])]
+   #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
+   (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
    [⊢ [τ_arg ≫ τ_arg- ⇐ : k_in] ...]
    --------
    [⊢ [_ ≫ (#%app- τ_fn- τ_arg- ...) ⇒ : k_out]]])
diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt
index b3ec142..e935c3b 100644
--- a/turnstile/examples/fomega2.rkt
+++ b/turnstile/examples/fomega2.rkt
@@ -88,7 +88,7 @@
   [(inst e τ ...) ≫
    [⊢ [e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
    [⊢ [τ ≫ τ- ⇐ : k] ...]
-   [#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)]
+   #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
    --------
    [⊢ [_ ≫ e- ⇒ : τ-inst]]])
 
diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt
index adf43bb..ff918e3 100644
--- a/turnstile/examples/fsub.rkt
+++ b/turnstile/examples/fsub.rkt
@@ -86,7 +86,7 @@
   [(inst e τ:type ...) ≫
    [⊢ [e ≫ e- ⇒ : (~∀ ([tv <: τ_sub] ...) τ_body)]]
    [τ.norm τ⊑ τ_sub #:for τ] ...
-   [#:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)]
+   #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)
    --------
    [⊢ [_ ≫ e- ⇒ : τ_inst]]])
 
diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt
index 1c3113a..14a4fc5 100644
--- a/turnstile/examples/infer.rkt
+++ b/turnstile/examples/infer.rkt
@@ -145,48 +145,48 @@
 
 (define-typed-syntax λ
   [(λ (x:id ...) body:expr) ≫
-   [#:with [X ...]
-    (for/list ([X (in-list (generate-temporaries #'[x ...]))])
-      (add-orig X X))]
+   #:with [X ...]
+   (for/list ([X (in-list (generate-temporaries #'[x ...]))])
+     (add-orig X X))
    [([X ≫ X- : #%type] ...) ([x ≫ x- : X] ...)
     ⊢ [body ≫ body- ⇒ : τ_body*]]
-   [#:with (~?Some [V ...] τ_body (~Cs [id_2 τ_2] ...)) (syntax-local-introduce #'τ_body*)]
-   [#:with τ_fn (some/inst/generalize #'[X- ... V ...]
-                                      #'(→ X- ... τ_body)
-                                      #'([id_2 τ_2] ...))]
+   #:with (~?Some [V ...] τ_body (~Cs [id_2 τ_2] ...)) (syntax-local-introduce #'τ_body*)
+   #:with τ_fn (some/inst/generalize #'[X- ... V ...]
+                                     #'(→ X- ... τ_body)
+                                     #'([id_2 τ_2] ...))
    --------
    [⊢ [_ ≫ (λ- (x- ...) body-) ⇒ : τ_fn]]])
 
 (define-typed-syntax #%app
   [(_ e_fn e_arg ...) ≫
-   [#:with [A ...] (generate-temporaries #'[e_arg ...])]
-   [#:with B (generate-temporary 'result)]
+   #:with [A ...] (generate-temporaries #'[e_arg ...])
+   #:with B (generate-temporary 'result)
    [⊢ [e_fn ≫ e_fn- ⇒ : τ_fn*]]
-   [#:with (~?Some [V1 ...] (~?∀ (V2 ...) τ_fn) (~Cs [τ_3 τ_4] ...))
-    (syntax-local-introduce #'τ_fn*)]
-   [#:with τ_fn-expected (tycons #'→ #'[A ... B])]
+   #:with (~?Some [V1 ...] (~?∀ (V2 ...) τ_fn) (~Cs [τ_3 τ_4] ...))
+   (syntax-local-introduce #'τ_fn*)
+   #:with τ_fn-expected (tycons #'→ #'[A ... B])
    [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg*] ...]
-   [#:with [(~?Some [V3 ...] (~?∀ (V4 ...) τ_arg) (~Cs [τ_5 τ_6] ...)) ...]
-    (syntax-local-introduce #'[τ_arg* ...])]
-   [#:with τ_out (some/inst/generalize #'[A ... B V1 ... V2 ... V3 ... ... V4 ... ...]
-                                       #'B
-                                       #'([τ_fn-expected τ_fn]
-                                          [τ_3 τ_4] ...
-                                          [A τ_arg] ...
-                                          [τ_5 τ_6] ... ...))]
+   #:with [(~?Some [V3 ...] (~?∀ (V4 ...) τ_arg) (~Cs [τ_5 τ_6] ...)) ...]
+   (syntax-local-introduce #'[τ_arg* ...])
+   #:with τ_out (some/inst/generalize #'[A ... B V1 ... V2 ... V3 ... ... V4 ... ...]
+                                      #'B
+                                      #'([τ_fn-expected τ_fn]
+                                         [τ_3 τ_4] ...
+                                         [A τ_arg] ...
+                                         [τ_5 τ_6] ... ...))
    --------
    [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]])
 
 (define-typed-syntax ann #:datum-literals (:)
   [(ann e:expr : τ:type) ≫
    [⊢ [e ≫ e- ⇒ : τ_e]]
-   [#:with (~?Some [V1 ...] (~?∀ (V2 ...) τ_fn) (~Cs [τ_1 τ_2] ...))
-    (syntax-local-introduce #'τ_e)]
-   [#:with τ_e* (some/inst/generalize #'[V1 ... V2 ...]
-                                      #'τ.norm
-                                      #'([τ.norm τ_e]
-                                         [τ_1 τ_2]
-                                         ...))]
+   #:with (~?Some [V1 ...] (~?∀ (V2 ...) τ_fn) (~Cs [τ_1 τ_2] ...))
+   (syntax-local-introduce #'τ_e)
+   #:with τ_e* (some/inst/generalize #'[V1 ... V2 ...]
+                                     #'τ.norm
+                                     #'([τ.norm τ_e]
+                                        [τ_1 τ_2]
+                                        ...))
    [τ_e* τ⊑ τ.norm #:for e]
    --------
    [⊢ [_ ≫ e- ⇒ : τ.norm]]])
@@ -194,7 +194,7 @@
 (define-typed-syntax define
   [(define x:id e:expr) ≫
    [⊢ [e ≫ e- ⇒ : τ_e]]
-   [#:with tmp (generate-temporary #'x)]
+   #:with tmp (generate-temporary #'x)
    --------
    [_ ≻ (begin-
           (define-syntax- x (make-rename-transformer (⊢ tmp : τ_e)))
@@ -202,7 +202,7 @@
 
 (define-typed-syntax define/rec #:datum-literals (:)
   [(define/rec x:id : τ_x:type e:expr) ≫
-   [#:with tmp (generate-temporary #'x)]
+   #:with tmp (generate-temporary #'x)
    --------
    [_ ≻ (begin-
           (define-syntax- x (make-rename-transformer (⊢ tmp : τ_x.norm)))
diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
index ab7ce32..07363f4 100644
--- a/turnstile/examples/mlish.rkt
+++ b/turnstile/examples/mlish.rkt
@@ -313,7 +313,7 @@
 (define-typed-syntax define
   [(define x:id e) ≫
    [⊢ [e ≫ e- ⇒ : τ]]
-   [#:with y (generate-temporary)]
+   #:with y (generate-temporary)
    --------
    [_ ≻ (begin-
           (define-syntax x (make-rename-transformer (⊢ y : τ)))
@@ -321,16 +321,16 @@
   ; explicit "forall"
   [(define Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) 
      e_body ... e) ≫
-   [#:when (brace? #'Ys)]
+   #:when (brace? #'Ys)
    ;; TODO; remove this code duplication
-   [#:with g (add-orig (generate-temporary #'f) #'f)]
-   [#:with e_ann #'(add-expected e τ_out)]
-   [#:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))]
+   #:with g (add-orig (generate-temporary #'f) #'f)
+   #:with e_ann #'(add-expected e τ_out)
+   #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
    ;; TODO: check that specified return type is correct
    ;; - currently cannot do it here; to do the check here, need all types of
    ;;  top-lvl fns, since they can call each other
-   [#:with (~and ty_fn_expected (~?∀ _ (~ext-stlc:→ _ ... out_expected))) 
-           ((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...)))]
+   #:with (~and ty_fn_expected (~?∀ _ (~ext-stlc:→ _ ... out_expected))) 
+          ((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...)))
    --------
    [_ ≻ (begin-
           (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected)))
@@ -342,18 +342,18 @@
    [_ ≻ (define (f [x : ty] ... -> ty_out) . b)]]
   [(define (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) 
      e_body ... e) ≫
-   [#:with Ys (compute-tyvars #'(τ ... τ_out))]
-   [#:with g (add-orig (generate-temporary #'f) #'f)]
-   [#:with e_ann (syntax/loc #'e (ann e : τ_out))] ; must be macro bc t_out may have unbound tvs
-   [#:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))]
+   #:with Ys (compute-tyvars #'(τ ... τ_out))
+   #:with g (add-orig (generate-temporary #'f) #'f)
+   #:with e_ann (syntax/loc #'e (ann e : τ_out)) ; must be macro bc t_out may have unbound tvs
+   #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
    ;; TODO: check that specified return type is correct
    ;; - currently cannot do it here; to do the check here, need all types of
    ;;  top-lvl fns, since they can call each other
-   [#:with (~and ty_fn_expected (~?∀ _ (~ext-stlc:→ _ ... out_expected))) 
-           (set-stx-prop/preserved 
-            ((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...)))
-            'orig
-            (list #'(→ τ+orig ...)))]
+   #:with (~and ty_fn_expected (~?∀ _ (~ext-stlc:→ _ ... out_expected))) 
+          (set-stx-prop/preserved 
+           ((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...)))
+           'orig
+           (list #'(→ τ+orig ...)))
    --------
    [_ ≻ (begin-
           (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected)))
@@ -462,36 +462,36 @@
            (syntax-parse/typed-syntax stx
              ; no args and not polymorphic
              [C:id ≫
-              [#:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...)))]
+              #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...)))
               --------
               [_ ≻ (C)]]
              ; no args but polymorphic, check expected type
              [C:id ⇐ : (NameExpander τ-expected-arg (... ...)) ≫
-              [#:when (stx-null? #'(τ ...))]
+              #:when (stx-null? #'(τ ...))
               --------
               [⊢ [_ ≫ (StructName) ⇐ : _]]]
              ; id with multiple expected args, HO fn
              [C:id ≫
-              [#:when (not (stx-null? #'(τ ...)))]
+              #:when (not (stx-null? #'(τ ...)))
               --------
               [⊢ [_ ≫ StructName ⇒ : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]]]
              [(C τs e_arg ...) ≫
-              [#:when (brace? #'τs)] ; commit to this clause
-              [#:with [X* (... ...)] #'[X ...]]
-              [#:with [e_arg* (... ...)] #'[e_arg ...]]
-              [#:with {~! τ_X:type (... ...)} #'τs]
-              [#:with (τ_in:type (... ...)) ; instantiated types
-               (inst-types/cs #'(X ...) #'([X* τ_X.norm] (... ...)) #'(τ ...))]
+              #:when (brace? #'τs) ; commit to this clause
+              #:with [X* (... ...)] #'[X ...]
+              #:with [e_arg* (... ...)] #'[e_arg ...]
+              #:with {~! τ_X:type (... ...)} #'τs
+              #:with (τ_in:type (... ...)) ; instantiated types
+              (inst-types/cs #'(X ...) #'([X* τ_X.norm] (... ...)) #'(τ ...))
               [⊢ [e_arg* ≫ e_arg*- ⇐ : τ_in.norm] (... ...)]
-              [#:with [e_arg- ...] #'[e_arg*- (... ...)]]
+              #:with [e_arg- ...] #'[e_arg*- (... ...)]
               --------
               [⊢ [_ ≫ (StructName e_arg- ...) ⇒ : (Name τ_X.norm (... ...))]]]
              [(C . args) ≫ ; no type annotations, must infer instantiation
-              [#:with StructName/ty 
-               (set-stx-prop/preserved
-                (⊢ StructName : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))
-                'orig
-                (list #'C))]
+              #:with StructName/ty 
+              (set-stx-prop/preserved
+               (⊢ StructName : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))
+               'orig
+               (list #'C))
               --------
               [_ ≻ (mlish:#%app StructName/ty . args)]]))
          ...)]))
@@ -678,18 +678,18 @@
 
 (define-typed-syntax match2 #:datum-literals (with ->)
   [(match2 e with . clauses) ≫
-   [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
+   #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"
    [⊢ [e ≫ e- ⇒ : τ_e]]
-   [#:with ([(~seq p ...) -> e_body] ...) #'clauses]
-   [#:with (pat ...) (stx-map ; use brace to indicate root pattern
-                      (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
-                      #'((p ...) ...)) ]
-   [#:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)]
-   [#:with ty-expected (get-expected-type stx)]
+   #:with ([(~seq p ...) -> e_body] ...) #'clauses
+   #:with (pat ...) (stx-map ; use brace to indicate root pattern
+                     (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
+                     #'((p ...) ...))
+   #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)
+   #:with ty-expected (get-expected-type stx)
    [() ([x ≫ x- : ty] ...)
     ⊢ [(add-expected e_body ty-expected) ≫ e_body- ⇒ : ty_body]]
    ...
-   [#:when (check-exhaust #'(pat- ...) #'τ_e)]
+   #:when (check-exhaust #'(pat- ...) #'τ_e)
    --------
    [⊢ [_ ≫ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...)
        ⇒ : (⊔ ty_body ...)]]])
@@ -697,55 +697,55 @@
 (define-typed-syntax match #:datum-literals (with -> ::)
   ;; e is a tuple
   [(match e with . clauses) ≫
-   [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
+   #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"
    [⊢ [e ≫ e- ⇒ : τ_e]]
-   [#:when (×? #'τ_e)]
-   [#:with t_expect (get-expected-type stx)] ; propagate inferred type
-   [#:with ([x ... -> e_body]) #'clauses]
-   [#:with (~× ty ...) #'τ_e]
-   [#:fail-unless (stx-length=? #'(ty ...) #'(x ...))
-                  "match clause pattern not compatible with given tuple"]
+   #:when (×? #'τ_e)
+   #:with t_expect (get-expected-type stx) ; propagate inferred type
+   #:with ([x ... -> e_body]) #'clauses
+   #:with (~× ty ...) #'τ_e
+   #:fail-unless (stx-length=? #'(ty ...) #'(x ...))
+                 "match clause pattern not compatible with given tuple"
    [() ([x ≫ x- : ty] ...)
     ⊢ [(add-expected e_body t_expect) ≫ e_body- ⇒ : ty_body]]
-   [#:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
-                       #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))]
-   [#:with z (generate-temporary)]
+   #:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
+                      #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))
+   #:with z (generate-temporary)
    --------
    [⊢ [_ ≫ (let- ([z e-])
              (let- ([x- (acc z)] ...) e_body-))
        ⇒ : ty_body]]]
   ;; e is a list
   [(match e with . clauses) ≫
-   [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
+   #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"
    [⊢ [e ≫ e- ⇒ : τ_e]]
-   [#:when (List? #'τ_e)]
-   [#:with t_expect (get-expected-type stx)] ; propagate inferred type
-   [#:with ([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
-                  (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'())))
-             -> e_body] ...+)
-    #'clauses]
-   [#:fail-unless (stx-ormap 
-                   (lambda (xx) (and (brack? xx) (zero? (stx-length xx)))) 
-                   #'(xs ...))
-    "match: missing empty list case"]
-   [#:fail-unless (not (and (stx-andmap brack? #'(xs ...))
-                            (= 1 (stx-length #'(xs ...)))))
-    "match: missing non-empty list case"]
-   [#:with (~List ty) #'τ_e]
+   #:when (List? #'τ_e)
+   #:with t_expect (get-expected-type stx) ; propagate inferred type
+   #:with ([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
+                 (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'())))
+            -> e_body] ...+)
+   #'clauses
+   #:fail-unless (stx-ormap 
+                  (lambda (xx) (and (brack? xx) (zero? (stx-length xx)))) 
+                  #'(xs ...))
+   "match: missing empty list case"
+   #:fail-unless (not (and (stx-andmap brack? #'(xs ...))
+                           (= 1 (stx-length #'(xs ...)))))
+   "match: missing non-empty list case"
+   #:with (~List ty) #'τ_e
    [() ([x ≫ x- : ty] ... [rst ≫ rst- : (List ty)])
     ⊢ [(add-expected e_body t_expect) ≫ e_body- ⇒ : ty_body]]
    ...
-   [#:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))]
-   [#:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...))]
-   [#:with (pred? ...) (stx-map
-                        (lambda (l lo) #`(λ- (lst) (#,lo (length lst) #,l)))
-                        #'(len ...) #'(lenop ...))]
-   [#:with ((acc1 ...) ...) (stx-map 
-                             (lambda (xs)
-                               (for/list ([(x i) (in-indexed (syntax->list xs))])
-                                 #`(lambda- (lst) (list-ref- lst #,(datum->syntax #'here i)))))
-                             #'((x ...) ...))]
-   [#:with (acc2 ...) (stx-map (lambda (l) #`(lambda- (lst) (list-tail- lst #,l))) #'(len ...))]
+   #:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))
+   #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...))
+   #:with (pred? ...) (stx-map
+                       (lambda (l lo) #`(λ- (lst) (#,lo (length lst) #,l)))
+                       #'(len ...) #'(lenop ...))
+   #:with ((acc1 ...) ...) (stx-map 
+                            (lambda (xs)
+                              (for/list ([(x i) (in-indexed (syntax->list xs))])
+                                #`(lambda- (lst) (list-ref- lst #,(datum->syntax #'here i)))))
+                            #'((x ...) ...))
+   #:with (acc2 ...) (stx-map (lambda (l) #`(lambda- (lst) (list-tail- lst #,l))) #'(len ...))
    --------
    [⊢ [_ ≫ (let- ([z e-])
              (cond-
@@ -754,47 +754,47 @@
        ⇒ : (⊔ ty_body ...)]]]
   ;; e is a variant
   [(match e with . clauses) ≫
-   [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
+   #:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"
    [⊢ [e ≫ e- ⇒ : τ_e]]
-   [#:when (and (not (×? #'τ_e)) (not (List? #'τ_e)))]
-   [#:with t_expect (get-expected-type stx)] ; propagate inferred type
-   [#:with ([Clause:id x:id ... 
-                       (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
-                       -> e_c_un] ...+) ; un = unannotated with expected ty
-    #'clauses]
+   #:when (and (not (×? #'τ_e)) (not (List? #'τ_e)))
+   #:with t_expect (get-expected-type stx) ; propagate inferred type
+   #:with ([Clause:id x:id ... 
+                      (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
+                      -> e_c_un] ...+) ; un = unannotated with expected ty
+   #'clauses
    ;; length #'clauses may be > length #'info, due to guards
-   [#:with info-body (get-extra-info #'τ_e)]
-   [#:with (_ (_ (_ ConsAll) . _) ...) #'info-body]
-   [#:fail-unless (set=? (syntax->datum #'(Clause ...))
-                         (syntax->datum #'(ConsAll ...)))
-    (type-error #:src stx
-                #:msg (string-append
-                       "match: clauses not exhaustive; missing: "
-                       (string-join      
-                        (map symbol->string
-                             (set-subtract 
-                              (syntax->datum #'(ConsAll ...))
-                              (syntax->datum #'(Clause ...))))
-                        ", ")))]
-   [#:with ((_ _ _ Cons? [_ acc τ] ...) ...)
-    (map ; ok to compare symbols since clause names can't be rebound
-     (lambda (Cl) 
-       (stx-findf
-        (syntax-parser
-          [(_ 'C . rst) (equal? Cl (syntax->datum #'C))])
-        (stx-cdr #'info-body))) ; drop leading #%app
-     (syntax->datum #'(Clause ...)))]
+   #:with info-body (get-extra-info #'τ_e)
+   #:with (_ (_ (_ ConsAll) . _) ...) #'info-body
+   #:fail-unless (set=? (syntax->datum #'(Clause ...))
+                        (syntax->datum #'(ConsAll ...)))
+   (type-error #:src stx
+               #:msg (string-append
+                      "match: clauses not exhaustive; missing: "
+                      (string-join      
+                       (map symbol->string
+                            (set-subtract 
+                             (syntax->datum #'(ConsAll ...))
+                             (syntax->datum #'(Clause ...))))
+                       ", ")))
+   #:with ((_ _ _ Cons? [_ acc τ] ...) ...)
+   (map ; ok to compare symbols since clause names can't be rebound
+    (lambda (Cl) 
+      (stx-findf
+       (syntax-parser
+         [(_ 'C . rst) (equal? Cl (syntax->datum #'C))])
+       (stx-cdr #'info-body))) ; drop leading #%app
+    (syntax->datum #'(Clause ...)))
    ;; this commented block experiments with expanding to unsafe ops
-   ;; [#:with ((acc ...) ...) (stx-map 
-   ;;                          (lambda (accs)
-   ;;                           (for/list ([(a i) (in-indexed (syntax->list accs))])
-   ;;                             #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
-   ;;                          #'((acc-fn ...) ...))]
-   [#:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))]
+   ;; #:with ((acc ...) ...) (stx-map 
+   ;;                         (lambda (accs)
+   ;;                          (for/list ([(a i) (in-indexed (syntax->list accs))])
+   ;;                            #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
+   ;;                         #'((acc-fn ...) ...))
+   #:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))
    [() ([x ≫ x- : τ] ...)
     ⊢ [e_guard ≫ e_guard- ⇐ : Bool] [e_c ≫ e_c- ⇒ : τ_ec]]
    ...
-   [#:with z (generate-temporary)] ; dont duplicate eval of test expr
+   #:with z (generate-temporary) ; dont duplicate eval of test expr
    --------
    [⊢ [_ ≫ (let- ([z e-])
              (cond-
@@ -837,15 +837,15 @@
 ; all λs have type (?∀ (X ...) (→ τ_in ... τ_out))
 (define-typed-syntax λ #:datum-literals (:)
   [(λ (x:id ...) body) ⇐ : (~?∀ (X ...) (~ext-stlc:→ τ_in ... τ_out)) ≫
-   [#:fail-unless (stx-length=? #'[x ...] #'[τ_in ...])
-    (format "expected a function of ~a arguments, got one with ~a arguments"
-            (stx-length #'[τ_in ...]) (stx-length #'[x ...]))]
+   #:fail-unless (stx-length=? #'[x ...] #'[τ_in ...])
+   (format "expected a function of ~a arguments, got one with ~a arguments"
+           (stx-length #'[τ_in ...]) (stx-length #'[x ...]))
    [([X ≫ X- : #%type] ...) ([x ≫ x- : τ_in] ...)
     ⊢ [body ≫ body- ⇐ : τ_out]]
    --------
    [⊢ [_ ≫ (λ- (x- ...) body-) ⇐ : _]]]
   [(λ ([x : τ_x] ...) body) ⇐ : (~?∀ (V ...) (~ext-stlc:→ τ_in ... τ_out)) ≫
-   [#:with [X ...] (compute-tyvars #'(τ_x ...))]
+   #:with [X ...] (compute-tyvars #'(τ_x ...))
    [([X ≫ X- : #%type] ...) ()
     ⊢ [τ_x ≫ τ_x- ⇐ : #%type] ...]
    [τ_in τ⊑ τ_x- #:for x] ...
@@ -855,13 +855,13 @@
    --------
    [⊢ [_ ≫ (λ- (x- ...) body-) ⇐ : _]]]
   [(λ ([x : τ_x] ...) body) ≫
-   [#:with [X ...] (compute-tyvars #'(τ_x ...))]
+   #:with [X ...] (compute-tyvars #'(τ_x ...))
    ;; TODO is there a way to have λs that refer to ids defined after them?
    [([X ≫ X- : #%type] ...) ([x ≫ x- : τ_x] ...)
     ⊢ [body ≫ body- ⇒ : τ_body]]
-   [#:with [τ_x* ...] (inst-types/cs #'[X ...] #'([X X-] ...) #'[τ_x ...])]
-   [#:with τ_fn (add-orig #'(?∀ (X- ...) (ext-stlc:→ τ_x* ... τ_body))
-                          #`(→ #,@(stx-map get-orig #'[τ_x* ...]) #,(get-orig #'τ_body)))]
+   #:with [τ_x* ...] (inst-types/cs #'[X ...] #'([X X-] ...) #'[τ_x ...])
+   #:with τ_fn (add-orig #'(?∀ (X- ...) (ext-stlc:→ τ_x* ... τ_body))
+                         #`(→ #,@(stx-map get-orig #'[τ_x* ...]) #,(get-orig #'τ_body)))
    --------
    [⊢ [_ ≫ (λ- (x- ...) body-) ⇒ : τ_fn]]])
 
@@ -872,30 +872,30 @@
    ;; compute fn type (ie ∀ and →)
    [⊢ [e_fn ≫ e_fn- ⇒ : (~?∀ Xs (~ext-stlc:→ . tyX_args))]]
    ;; solve for type variables Xs
-   [#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args stx)]
+   #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args stx)
    ;; instantiate polymorphic function type
-   [#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)]
-   [#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)]
+   #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
+   #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
    ;; arity check
-   [#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
-    (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])]
+   #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+   (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
    ;; compute argument types
-   [#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))]
+   #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
    ;; typecheck args
    [τ_arg τ⊑ τ_in #:for e_arg] ...
-   [#:with τ_out* (if (stx-null? #'(unsolved-X ...))
-                      #'τ_out
-                      (syntax-parse #'τ_out
-                        [(~?∀ (Y ...) τ_out)
-                         #:fail-unless (→? #'τ_out)
-                         (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)
-                         (for ([X (in-list (syntax->list #'(unsolved-X ...)))])
-                           (unless (covariant-X? X #'τ_out)
-                             (raise-syntax-error
-                              #f
-                              (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)
-                              stx)))
-                         #'(∀ (unsolved-X ... Y ...) τ_out)]))]
+   #:with τ_out* (if (stx-null? #'(unsolved-X ...))
+                     #'τ_out
+                     (syntax-parse #'τ_out
+                       [(~?∀ (Y ...) τ_out)
+                        #:fail-unless (→? #'τ_out)
+                        (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)
+                        (for ([X (in-list (syntax->list #'(unsolved-X ...)))])
+                          (unless (covariant-X? X #'τ_out)
+                            (raise-syntax-error
+                             #f
+                             (mk-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)
+                             stx)))
+                        #'(∀ (unsolved-X ... Y ...) τ_out)]))
    --------
    [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out*]]])
 
@@ -935,7 +935,7 @@
 
 (define-typed-syntax make-channel
   [(make-channel (~and tys {ty})) ≫
-   [#:when (brace? #'tys)]
+   #:when (brace? #'tys)
    --------
    [⊢ [_ ≫ (make-channel-) ⇒ : (Channel ty)]]])
 (define-typed-syntax channel-get
@@ -996,7 +996,7 @@
 
 (define-typed-syntax vector
   [(vector (~and tys {ty})) ≫
-   [#:when (brace? #'tys)]
+   #:when (brace? #'tys)
    --------
    [⊢ [_ ≫ (vector-) ⇒ : (Vector ty)]]]
   [(vector v ...) ⇐ : (Vector ty) ≫
@@ -1005,8 +1005,8 @@
    [⊢ [_ ≫ (vector- v- ...) ⇐ : _]]]
   [(vector v ...) ≫
    [⊢ [v ≫ v- ⇒ : ty] ...]
-   [#:when (same-types? #'(ty ...))]
-   [#:with one-ty (stx-car #'(ty ...))]
+   #:when (same-types? #'(ty ...))
+   #:with one-ty (stx-car #'(ty ...))
    --------
    [⊢ [_ ≫ (vector- v- ...) ⇒ : (Vector one-ty)]]])
 (define-typed-syntax make-vector
@@ -1247,16 +1247,16 @@
 ; mutable hashes
 (define-typed-syntax hash
   [(hash (~and tys {ty_key ty_val})) ≫
-   [#:when (brace? #'tys)]
+   #:when (brace? #'tys)
    --------
    [⊢ [_ ≫ (make-hash-) ⇒ : (Hash ty_key ty_val)]]]
   [(hash (~seq k v) ...) ≫
    [⊢ [k ≫ k- ⇒ : ty_k] ...]
    [⊢ [v ≫ v- ⇒ : ty_v] ...]
-   [#:when (same-types? #'(ty_k ...))]
-   [#:when (same-types? #'(ty_v ...))]
-   [#:with ty_key (stx-car #'(ty_k ...))]
-   [#:with ty_val (stx-car #'(ty_v ...))]
+   #:when (same-types? #'(ty_k ...))
+   #:when (same-types? #'(ty_v ...))
+   #:with ty_key (stx-car #'(ty_k ...))
+   #:with ty_val (stx-car #'(ty_v ...))
    --------
    [⊢ [_ ≫ (make-hash- (list- (cons- k- v-) ...)) ⇒ : (Hash ty_key ty_val)]]])
 (define-typed-syntax hash-set!
@@ -1368,7 +1368,7 @@
   [(provide x:id ...) ≫
    [⊢ [x ≫ x- ⇒ : ty_x] ...]
    ; TODO: use hash-code to generate this tmp
-   [#:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))]
+   #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
    --------
    [_ ≻ (begin-
           (provide- x ...)
@@ -1376,8 +1376,8 @@
           (provide- x-ty ...))]])
 (define-typed-syntax require-typed
   [(require-typed x:id ... #:from mod) ≫
-   [#:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))]
-   [#:with (y ...) (generate-temporaries #'(x ...))]
+   #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
+   #:with (y ...) (generate-temporaries #'(x ...))
    --------
    [_ ≻ (begin-
           (require- (rename-in (only-in mod x ... x-ty ...) [x y] ...))
diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
index 04dc199..75281c3 100644
--- a/turnstile/examples/rosette/bv.rkt
+++ b/turnstile/examples/rosette/bv.rkt
@@ -61,10 +61,10 @@
    [_ ≻ (define-fragment (id param ...) #:implements spec #:library lib-expr #:minbv (rosette:#%datum . 4))]]
   [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv) ≫
    [⊢ [spec ≫ spec- ⇒ : ty_spec]]
-   [#:fail-unless (→? #'ty_spec) "spec must be a function"]
+   #:fail-unless (→? #'ty_spec) "spec must be a function"
    [⊢ [lib-expr ≫ lib-expr- ⇐ : Lib]]
    [⊢ [minbv ≫ minbv- ⇐ : Int]]
-   [#:with id-stx (format-id #'id "~a-stx" #'id #:source #'id)]
+   #:with id-stx (format-id #'id "~a-stx" #'id #:source #'id)
    --------
    [_ ≻ (begin-
             (define-values- (id-internal id-stx-internal)
@@ -78,15 +78,15 @@
 
 (define-typed-syntax bvlib
   [(_ [(~and ids (id ...)) n] ...) ≫
-   [#:fail-unless (stx-andmap brace? #'(ids ...))
-                  "given ops must be enclosed with braces"]
+   #:fail-unless (stx-andmap brace? #'(ids ...))
+                 "given ops must be enclosed with braces"
    [⊢ [n ≫ n- ⇐ : Int] ...]
    [⊢ [id ≫ id- ⇒ : ty_id] ... ...]
-   [#:fail-unless (stx-andmap →? #'(ty_id ... ...))
-                  "given op must be a function"]
-   [#:with ((~→ ty ...) ...) #'(ty_id ... ...)]
-   [#:fail-unless (stx-andmap BV? #'(ty ... ...))
-                  "given op must have BV inputs and output"]
+   #:fail-unless (stx-andmap →? #'(ty_id ... ...))
+                 "given op must be a function"
+   #:with ((~→ ty ...) ...) #'(ty_id ... ...)
+   #:fail-unless (stx-andmap BV? #'(ty ... ...))
+                 "given op must have BV inputs and output"
    --------
    [⊢ [_ ≫ (bv:bvlib [{id- ...} n-] ...) ⇒ : Lib]]])
 
diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt
index 05fdcb4..b8f31a5 100644
--- a/turnstile/examples/rosette/fsm.rkt
+++ b/turnstile/examples/rosette/fsm.rkt
@@ -23,16 +23,16 @@
 (define-typed-syntax automaton #:datum-literals (: →)
   [(_ init-state:id
       [state:id : (label:id → target) ...] ...) ≫
-   [#:fail-unless (member (syntax->datum #'init-state)
-                          (syntax->datum #'(state ...)))
-                  (format "initial state ~a is not declared state: ~a"
-                          (syntax->datum #'init-state)
-                          (syntax->datum #'(state ...)))]
-   #;[#:fail-unless (let ([states (syntax->datum #'(state ...))])
-                    (for/and ([t (syntax->datum #'(target ... ...))])
-                      (member t states)))
-                  (format "transition to unknown state")]
-   [#:with arr (datum->syntax #f '→)]
+   #:fail-unless (member (syntax->datum #'init-state)
+                         (syntax->datum #'(state ...)))
+                 (format "initial state ~a is not declared state: ~a"
+                         (syntax->datum #'init-state)
+                         (syntax->datum #'(state ...)))
+   ;#:fail-unless (let ([states (syntax->datum #'(state ...))])
+   ;                (for/and ([t (syntax->datum #'(target ... ...))])
+   ;                  (member t states)))
+   ;              (format "transition to unknown state")
+   #:with arr (datum->syntax #f '→)
    [() ([state ≫ state- : State] ...) ⊢ 
     [init-state ≫ init-state- ⇐ : State]
     [target ≫ target- ⇐ : State] ... ...]
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
index 9403a78..6624187 100644
--- a/turnstile/examples/rosette/rosette.rkt
+++ b/turnstile/examples/rosette/rosette.rkt
@@ -21,7 +21,7 @@
 (define-typed-syntax define-symbolic
   [(_ x:id ...+ pred : ty:type) ≫
    [⊢ [pred ≫ pred- ⇐ : (→ ty.norm Bool)]]
-   [#:with (y ...) (generate-temporaries #'(x ...))]
+   #:with (y ...) (generate-temporaries #'(x ...))
    --------
    [_ ≻ (begin-
           (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ...
@@ -85,7 +85,7 @@
    [_ ≻ (stlc:define x e)]]
   [(_ (f [x : ty] ... (~or → ->) ty_out) e) ≫
 ;   [⊢ [e ≫ e- ⇒ : ty_e]]
-   [#:with f- (generate-temporary #'f)]
+   #:with f- (generate-temporary #'f)
    --------
    [_ ≻ (begin-
           (define-syntax- f (make-rename-transformer (⊢ f- : (→ ty ... ty_out))))
diff --git a/turnstile/examples/stlc+cons.rkt b/turnstile/examples/stlc+cons.rkt
index 024e0fe..23fdcfc 100644
--- a/turnstile/examples/stlc+cons.rkt
+++ b/turnstile/examples/stlc+cons.rkt
@@ -39,8 +39,8 @@
 (define-typed-syntax tail
   [(tail e) ≫
    [⊢ [e ≫ e- ⇒ : τ-lst]]
-   [#:fail-unless (List? #'τ-lst)
-    (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
+   #:fail-unless (List? #'τ-lst)
+   (format "Expected a list type, got: ~a" (type->str #'τ-lst))
    --------
    [⊢ [_ ≫ (cdr- e-) ⇒ : τ-lst]]])
 (define-typed-syntax list
@@ -56,15 +56,15 @@
 (define-typed-syntax reverse
   [(reverse e) ≫
    [⊢ [e ≫ e- ⇒ : τ-lst]]
-   [#:fail-unless (List? #'τ-lst)
-    (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
+   #:fail-unless (List? #'τ-lst)
+   (format "Expected a list type, got: ~a" (type->str #'τ-lst))
    --------
    [⊢ [_ ≫ (reverse- e-) ⇒ : τ-lst]]])
 (define-typed-syntax length
   [(length e) ≫
    [⊢ [e ≫ e- ⇒ : τ-lst]]
-   [#:fail-unless (List? #'τ-lst)
-    (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
+   #:fail-unless (List? #'τ-lst)
+   (format "Expected a list type, got: ~a" (type->str #'τ-lst))
    --------
    [⊢ [_ ≫ (length- e-) ⇒ : Int]]])
 (define-typed-syntax list-ref
diff --git a/turnstile/examples/stlc+effect.rkt b/turnstile/examples/stlc+effect.rkt
index f29b842..775e338 100644
--- a/turnstile/examples/stlc+effect.rkt
+++ b/turnstile/examples/stlc+effect.rkt
@@ -38,8 +38,8 @@
        (⇒ ν (~locs fns ...))
        (⇒ := (~locs fas ...))
        (⇒ ! (~locs fds ...))]]
-   [#:fail-unless (stx-length=? #'[e ...] #'[τ_in ...])
-    (num-args-fail-msg #'efn #'[τ_in ...] #'[e ...])]
+   #:fail-unless (stx-length=? #'[e ...] #'[τ_in ...])
+   (num-args-fail-msg #'efn #'[τ_in ...] #'[e ...])
    [⊢ [e ≫ e_arg-
        (⇐ : τ_in)
        (⇒ ν (~locs ns ...))
diff --git a/turnstile/examples/stlc+rec-iso.rkt b/turnstile/examples/stlc+rec-iso.rkt
index 05fa936..278ba66 100644
--- a/turnstile/examples/stlc+rec-iso.rkt
+++ b/turnstile/examples/stlc+rec-iso.rkt
@@ -38,14 +38,14 @@
 
 (define-typed-syntax unfld
   [(unfld τ:type-ann e) ≫
-   [#:with (~μ* (tv) τ_body) #'τ.norm]
+   #:with (~μ* (tv) τ_body) #'τ.norm
    [⊢ [e ≫ e- ⇐ : τ.norm]]
    --------
    [⊢ [_ ≫ e- ⇒ : #,(subst #'τ.norm #'tv #'τ_body)]]])
 (define-typed-syntax fld
   [(fld τ:type-ann e) ≫
-   [#:with (~μ* (tv) τ_body) #'τ.norm]
-   [#:with τ_e (subst #'τ.norm #'tv #'τ_body)]
+   #:with (~μ* (tv) τ_body) #'τ.norm
+   #:with τ_e (subst #'τ.norm #'tv #'τ_body)
    [⊢ [e ≫ e- ⇐ : τ_e]]
    --------
    [⊢ [_ ≫ e- ⇒ : τ.norm]]])
diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt
index cbcd295..bd1bf8b 100644
--- a/turnstile/examples/stlc+reco+var.rkt
+++ b/turnstile/examples/stlc+reco+var.rkt
@@ -39,7 +39,7 @@
           (define- y (ann e : τ.norm)))]]
   [(define x:id e) ≫
    [⊢ [e ≫ e- ⇒ : τ]]
-   [#:with y (generate-temporary #'x)]
+   #:with y (generate-temporary #'x)
    --------
    [_ ≻ (begin-
           (define-syntax x (make-rename-transformer (⊢ y : τ)))
@@ -95,10 +95,10 @@
 (define-typed-syntax proj #:literals (quote)
   [(proj e_rec l:id) ≫
    [⊢ [e_rec ≫ e_rec- ⇒ : τ_e]]
-   [#:fail-unless (×? #'τ_e)
-    (format "Expected expression ~s to have × type, got: ~a"
-            (syntax->datum #'e_rec) (type->str #'τ_e))]
-   [#:with τ_l (×-ref #'τ_e #'l)]
+   #:fail-unless (×? #'τ_e)
+   (format "Expected expression ~s to have × type, got: ~a"
+           (syntax->datum #'e_rec) (type->str #'τ_e))
+   #:with τ_l (×-ref #'τ_e #'l)
    --------
    [⊢ [_ ≫ (cadr- (assoc- 'l e_rec-)) ⇒ : τ_l]]])
 
@@ -150,13 +150,13 @@
    --------
    [_ ≻ (ann (var l = e) : τ.norm)]]
   [(var l:id = e) ⇐ : τ ≫
-   [#:fail-unless (∨? #'τ)
-    (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ))]
-   [#:with τ_e
-    (∨-ref #'τ #'l #:else
-           (λ () (raise-syntax-error #f
-                    (format "~a field does not exist" (syntax->datum #'l))
-                    stx)))]
+   #:fail-unless (∨? #'τ)
+   (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ))
+   #:with τ_e
+   (∨-ref #'τ #'l #:else
+          (λ () (raise-syntax-error #f
+                   (format "~a field does not exist" (syntax->datum #'l))
+                   stx)))
    [⊢ [e ≫ e- ⇐ : τ_e]]
    --------
    [⊢ [_ ≫ (list- 'l e) ⇐ : _]]])
@@ -164,10 +164,10 @@
 (define-typed-syntax case
   #:datum-literals (of =>)
   [(case e [l:id x:id => e_l] ...) ≫
-   [#:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses"]
+   #:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses"
    [⊢ [e ≫ e- ⇒ : (~∨* [l_x : τ_x] ...)]]
-   [#:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses"]
-   [#:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"]
+   #:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses"
+   #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
    [() ([x ≫ x- : τ_x]) ⊢ [e_l ≫ e_l- ⇒ : τ_el]] ...
    --------
    [⊢ [_ ≫
diff --git a/turnstile/examples/stlc+tup.rkt b/turnstile/examples/stlc+tup.rkt
index 75adea4..d0312e6 100644
--- a/turnstile/examples/stlc+tup.rkt
+++ b/turnstile/examples/stlc+tup.rkt
@@ -17,7 +17,7 @@
 
 (define-typed-syntax tup
   [(tup e ...) ⇐ : (~× τ ...) ≫
-   [#:when (stx-length=? #'[e ...] #'[τ ...])]
+   #:when (stx-length=? #'[e ...] #'[τ ...])
    [⊢ [e ≫ e- ⇐ : τ] ...]
    --------
    [⊢ [_ ≫ (list- e- ...) ⇐ : _]]]
@@ -29,7 +29,7 @@
 (define-typed-syntax proj
   [(proj e_tup n:nat) ≫
    [⊢ [e_tup ≫ e_tup- ⇒ : (~× τ ...)]]
-   [#:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large"]
+   #:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large"
    --------
    [⊢ [_ ≫ (list-ref- e_tup- n) ⇒ : #,(stx-list-ref #'[τ ...] (syntax-e #'n))]]])
 
diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt
index 4cbace5..2975dbf 100644
--- a/turnstile/examples/stlc.rkt
+++ b/turnstile/examples/stlc.rkt
@@ -40,8 +40,8 @@
 (define-typed-syntax #%app
   [(_ e_fn e_arg ...) ≫
    [⊢ [e_fn ≫ e_fn- ⇒ : (~→ τ_in ... τ_out)]]
-   [#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
-    (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])]
+   #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+   (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
    [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...]
    --------
    [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]])
diff --git a/turnstile/examples/sysf.rkt b/turnstile/examples/sysf.rkt
index aa583a0..106900b 100644
--- a/turnstile/examples/sysf.rkt
+++ b/turnstile/examples/sysf.rkt
@@ -23,7 +23,7 @@
 (define-typed-syntax inst
   [(inst e τ:type ...) ≫
    [⊢ [e ≫ e- ⇒ : (~∀ tvs τ_body)]]
-   [#:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)]
+   #:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)
    --------
    [⊢ [_ ≫ e- ⇒ : τ_inst]]]
   [(inst e) ≫
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
index a7ee57e..13c9f4a 100644
--- a/turnstile/turnstile.rkt
+++ b/turnstile/turnstile.rkt
@@ -234,13 +234,13 @@
              #'(~post
                 (~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
                        (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))]
-    [pattern [#:when condition:expr]
+    [pattern (~seq #:when condition:expr)
              #:with pat
              #'(~fail #:unless condition)]
-    [pattern [#:with pat*:expr expr:expr]
+    [pattern (~seq #:with pat*:expr expr:expr)
              #:with pat
              #'(~post (~parse pat* expr))]
-    [pattern [#:fail-unless condition:expr message:expr]
+    [pattern (~seq #:fail-unless condition:expr message:expr)
              #:with pat
              #'(~post (~fail #:unless condition message))]
     )