diff --git a/tapl/typed-lang-builder/exist.rkt b/tapl/typed-lang-builder/exist.rkt
index 30292b5..a86f298 100644
--- a/tapl/typed-lang-builder/exist.rkt
+++ b/tapl/typed-lang-builder/exist.rkt
@@ -15,7 +15,7 @@
 (define-type-constructor ∃ #:bvs = 1)
 
 (define-typed-syntax pack
-  [(pack (τ:type e) as ∃τ:type) ▶
+  [(pack (τ:type e) as ∃τ:type) ≫
    [#:with (~∃* (τ_abstract) τ_body) #'∃τ.norm]
    [#:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body)]
    [⊢ [[e ≫ e-] ⇐ : τ_e]]
@@ -24,7 +24,7 @@
 
 (define-typed-syntax open #:datum-literals (<= with)
   [(open [x:id <= e_packed with X:id] e)
-   ▶
+   ≫
    ;; The subst below appears to be a hack, but it's not really.
    ;; It's the (TaPL) type rule itself that is fast and loose.
    ;; Leveraging the macro system's management of binding reveals this.
diff --git a/tapl/typed-lang-builder/ext-stlc.rkt b/tapl/typed-lang-builder/ext-stlc.rkt
index a08a15d..0a3ab46 100644
--- a/tapl/typed-lang-builder/ext-stlc.rkt
+++ b/tapl/typed-lang-builder/ext-stlc.rkt
@@ -23,20 +23,20 @@
 (define-base-type Char)
 
 (define-typed-syntax #%datum
-  [(#%datum . b:boolean) ▶
+  [(#%datum . b:boolean) ≫
    --------
    [⊢ [[_ ≫ (#%datum- . b)] ⇒ : Bool]]]
-  [(#%datum . s:str) ▶
+  [(#%datum . s:str) ≫
    --------
    [⊢ [[_ ≫ (#%datum- . s)] ⇒ : String]]]
-  [(#%datum . f) ▶
+  [(#%datum . f) ≫
    [#:when (flonum? (syntax-e #'f))]
    --------
    [⊢ [[_ ≫ (#%datum- . f)] ⇒ : Float]]]
-  [(#%datum . c:char) ▶
+  [(#%datum . c:char) ≫
    --------
    [⊢ [[_ ≫ (#%datum- . c)] ⇒ : Char]]]
-  [(#%datum . x) ▶
+  [(#%datum . x) ≫
    --------
    [_ ≻ (stlc+lit:#%datum . x)]])
 
@@ -48,14 +48,14 @@
 (define-primop not : (→ Bool Bool))
 
 (define-typed-syntax and
-  [(and e1 e2) ▶
+  [(and e1 e2) ≫
    [⊢ [[e1 ≫ e1-] ⇐ : Bool]]
    [⊢ [[e2 ≫ e2-] ⇐ : Bool]]
    --------
    [⊢ [[_ ≫ (and- e1- e2-)] ⇒ : Bool]]])
 
 (define-typed-syntax or
-  [(or e ...) ▶
+  [(or e ...) ≫
    [⊢ [[e ≫ e-] ⇐ : Bool] ...]
    --------
    [⊢ [[_ ≫ (or- e- ...)] ⇒ : Bool]]])
@@ -78,13 +78,13 @@
        ((current-join) τ τ2))]))
 
 (define-typed-syntax if
-  [(if e_tst e1 e2) ⇐ : τ-expected ▶
+  [(if e_tst e1 e2) ⇐ : τ-expected ≫
    [⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
    [⊢ [[e1 ≫ e1-] ⇐ : τ-expected]]
    [⊢ [[e2 ≫ e2-] ⇐ : τ-expected]]
    --------
    [⊢ [[_ ≫ (if- e_tst- e1- e2-)] ⇐ : _]]]
-  [(if e_tst e1 e2) ▶
+  [(if e_tst e1 e2) ≫
    [⊢ [[e_tst ≫ e_tst-] ⇒ : _]] ; Any non-false value is truthy.
    [⊢ [[e1 ≫ e1-] ⇒ : τ1]]
    [⊢ [[e2 ≫ e2-] ⇒ : τ2]]
@@ -95,24 +95,24 @@
 (define-primop void : (→ Unit))
 
 (define-typed-syntax begin
-  [(begin e_unit ... e) ⇐ : τ_expected ▶
+  [(begin e_unit ... e) ⇐ : τ_expected ≫
    [⊢ [[e_unit ≫ e_unit-] ⇒ : _] ...]
    [⊢ [[e ≫ e-] ⇐ : τ_expected]]
    --------
    [⊢ [[_ ≫ (begin- e_unit- ... e-)] ⇐ : _]]]
-  [(begin e_unit ... e) ▶
+  [(begin e_unit ... e) ≫
    [⊢ [[e_unit ≫ e_unit-] ⇒ : _] ...]
    [⊢ [[e ≫ e-] ⇒ : τ_e]]
    --------
    [⊢ [[_ ≫ (begin- e_unit- ... e-)] ⇒ : τ_e]]])
 
 (define-typed-syntax let
-  [(let ([x e] ...) e_body) ⇐ : τ_expected ▶
+  [(let ([x e] ...) e_body) ⇐ : τ_expected ≫
    [⊢ [[e ≫ e-] ⇒ : τ_x] ...]
    [() ([x : τ_x ≫ x-] ...) ⊢ [[e_body ≫ e_body-] ⇐ : τ_expected]]
    --------
    [⊢ [[_ ≫ (let- ([x- e-] ...) e_body-)] ⇐ : _]]]
-  [(let ([x e] ...) e_body) ▶
+  [(let ([x e] ...) e_body) ≫
    [⊢ [[e ≫ e-] ⇒ : τ_x] ...]
    [() ([x : τ_x ≫ x-] ...) ⊢ [[e_body ≫ e_body-] ⇒ : τ_body]]
    --------
@@ -123,20 +123,20 @@
 ; - only need to transfer expected type when local expanding an expression
 ;   - see let/tc
 (define-typed-syntax let*
-  [(let* () e_body) ▶
+  [(let* () e_body) ≫
    --------
    [_ ≻ e_body]]
-  [(let* ([x e] [x_rst e_rst] ...) e_body) ▶
+  [(let* ([x e] [x_rst e_rst] ...) e_body) ≫
    --------
    [_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body))]])
 
 (define-typed-syntax letrec
-  [(letrec ([b:type-bind e] ...) e_body) ⇐ : τ_expected ▶
+  [(letrec ([b:type-bind e] ...) e_body) ⇐ : τ_expected ≫
    [() ([b.x : b.type ≫ x-] ...)
     ⊢ [[e ≫ e-] ⇐ : b.type] ... [[e_body ≫ e_body-] ⇐ : τ_expected]]
    --------
    [⊢ [[_ ≫ (letrec- ([x- e-] ...) e_body-)] ⇐ : _]]]
-  [(letrec ([b:type-bind e] ...) e_body) ▶
+  [(letrec ([b:type-bind e] ...) e_body) ≫
    [() ([b.x : b.type ≫ x-] ...)
     ⊢ [[e ≫ e-] ⇐ : b.type] ... [[e_body ≫ e_body-] ⇒ : τ_body]]
    --------
diff --git a/tapl/typed-lang-builder/fomega.rkt b/tapl/typed-lang-builder/fomega.rkt
index 5bf58c8..16937b4 100644
--- a/tapl/typed-lang-builder/fomega.rkt
+++ b/tapl/typed-lang-builder/fomega.rkt
@@ -83,13 +83,13 @@
   (current-typecheck-relation (current-type=?)))
 
 (define-typed-syntax Λ
-  [(Λ bvs:kind-ctx e) ▶
+  [(Λ bvs:kind-ctx e) ≫
    [([bvs.x : bvs.kind ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ : τ_e]]
    --------
    [⊢ [[_ ≫ e-] ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
 
 (define-typed-syntax inst
-  [(inst e τ ...) ▶
+  [(inst e τ ...) ≫
    [⊢ [[e ≫ e-] ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
    [⊢ [[τ ≫ τ-] ⇐ : k] ...]
    [#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)]
@@ -99,7 +99,7 @@
 ;; TODO: merge with regular λ and app?
 ;; - see fomega2.rkt
 (define-typed-syntax tyλ
-  [(tyλ bvs:kind-ctx τ_body) ▶
+  [(tyλ bvs:kind-ctx τ_body) ≫
    [() ([bvs.x : bvs.kind ≫ tv-] ...) ⊢ [[τ_body ≫ τ_body-] ⇒ : k_body]]
    [#:fail-unless ((current-kind?) #'k_body)
     (format "not a valid type: ~a\n" (type->str #'τ_body))]
@@ -107,7 +107,7 @@
    [⊢ [[_ ≫ (λ- (tv- ...) τ_body-)] ⇒ : (⇒ bvs.kind ... k_body)]]])
 
 (define-typed-syntax tyapp
-  [(tyapp τ_fn τ_arg ...) ▶
+  [(tyapp τ_fn τ_arg ...) ≫
    [⊢ [[τ_fn ≫ τ_fn-] ⇒ : (~⇒ k_in ... k_out)]]
    [#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
     (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])]
diff --git a/tapl/typed-lang-builder/fomega2.rkt b/tapl/typed-lang-builder/fomega2.rkt
index d152435..93bb837 100644
--- a/tapl/typed-lang-builder/fomega2.rkt
+++ b/tapl/typed-lang-builder/fomega2.rkt
@@ -79,13 +79,13 @@
   (current-typecheck-relation (current-type=?)))
 
 (define-typed-syntax Λ
-  [(Λ bvs:kind-ctx e) ▶
+  [(Λ bvs:kind-ctx e) ≫
    [() ([bvs.x : bvs.kind ≫ tv-] ...) ⊢ [[e ≫ e-] ⇒ : τ_e]]
    --------
    [⊢ [[_ ≫ e-] ⇒ : (∀ ([tv- : bvs.kind] ...) τ_e)]]])
 
 (define-typed-syntax inst
-  [(inst e τ ...) ▶
+  [(inst e τ ...) ≫
    [⊢ [[e ≫ e-] ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]]
    [⊢ [[τ ≫ τ-] ⇐ : k] ...]
    [#:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)]
diff --git a/tapl/typed-lang-builder/fsub.rkt b/tapl/typed-lang-builder/fsub.rkt
index 1ff395b..4db0492 100644
--- a/tapl/typed-lang-builder/fsub.rkt
+++ b/tapl/typed-lang-builder/fsub.rkt
@@ -45,7 +45,7 @@
 ;; Problem: need type annotations, even in expanded form
 ;; Solution: store type annotations in a (quasi) kind <:
 (define-typed-syntax ∀ #:datum-literals (<:)
-  [(∀ ([tv:id <: τ:type] ...) τ_body) ▶
+  [(∀ ([tv:id <: τ:type] ...) τ_body) ≫
    --------
    ; eval first to overwrite the old #%type
    [⊢ [[_ ≫ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body))] ⇒ : (<: τ.norm ...)]]])
@@ -74,7 +74,7 @@
                        #:msg "Expected ∀ type, got: ~a" #'any))))]))))
 
 (define-typed-syntax Λ #:datum-literals (<:)
-  [(Λ ([tv:id <: τsub:type] ...) e) ▶
+  [(Λ ([tv:id <: τsub:type] ...) e) ≫
    ;; NOTE: store the subtyping relation of tv and τsub in the
    ;; environment with a syntax property using another tag: '<:
    ;; The "expose" function looks for this tag to enforce the bound,
@@ -83,7 +83,7 @@
    --------
    [⊢ [[_ ≫ e-] ⇒ : (∀ ([tv- <: τsub] ...) τ_e)]]])
 (define-typed-syntax inst
-  [(inst e τ:type ...) ▶
+  [(inst e τ:type ...) ≫
    [⊢ [[e ≫ e-] ⇒ : (~∀ ([tv <: τ_sub] ...) τ_body)]]
    [τ.norm τ⊑ τ_sub] ...
    [#:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)]
diff --git a/tapl/typed-lang-builder/mlish.rkt b/tapl/typed-lang-builder/mlish.rkt
index 32e3da8..36660b8 100644
--- a/tapl/typed-lang-builder/mlish.rkt
+++ b/tapl/typed-lang-builder/mlish.rkt
@@ -311,7 +311,7 @@
 ;;   which is not known to programmers, to make the result slightly more
 ;;   intuitive, we arbitrarily sort the inferred tyvars lexicographically
 (define-typed-syntax define
-  [(define x:id e) ▶
+  [(define x:id e) ≫
    [⊢ [[e ≫ e-] ⇒ : τ]]
    [#:with y (generate-temporary)]
    --------
@@ -320,7 +320,7 @@
           (define- y e-))]]
   ; explicit "forall"
   [(define Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) 
-     e_body ... e) ▶
+     e_body ... e) ≫
    [#:when (brace? #'Ys)]
    ;; TODO; remove this code duplication
    [#:with g (add-orig (generate-temporary #'f) #'f)]
@@ -337,11 +337,11 @@
           (define- g
             (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]]
   ;; alternate type sig syntax, after parameter names
-  [(define (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) ▶
+  [(define (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) ≫
    --------
    [_ ≻ (define (f [x : ty] ... -> ty_out) . b)]]
   [(define (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) 
-     e_body ... e) ▶
+     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
@@ -461,21 +461,21 @@
          (define-syntax (Cons stx)
            (syntax-parse/typed-syntax stx
              ; no args and not polymorphic
-             [C:id ▶
+             [C:id ≫
               [#:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...)))]
               --------
               [_ ≻ (C)]]
              ; no args but polymorphic, check expected type
-             [C:id ⇐ : (NameExpander τ-expected-arg (... ...)) ▶
+             [C:id ⇐ : (NameExpander τ-expected-arg (... ...)) ≫
               [#:when (stx-null? #'(τ ...))]
               --------
               [⊢ [[_ ≫ (StructName)] ⇐ : _]]]
              ; id with multiple expected args, HO fn
-             [C:id ▶
+             [C:id ≫
               [#:when (not (stx-null? #'(τ ...)))]
               --------
               [⊢ [[_ ≫ StructName] ⇒ : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]]]
-             [(C τs e_arg ...) ▶
+             [(C τs e_arg ...) ≫
               [#:when (brace? #'τs)] ; commit to this clause
               [#:with [X* (... ...)] #'[X ...]]
               [#:with [e_arg* (... ...)] #'[e_arg ...]]
@@ -486,7 +486,7 @@
               [#:with [e_arg- ...] #'[e_arg*- (... ...)]]
               --------
               [⊢ [[_ ≫ (StructName e_arg- ...)] ⇒ : (Name τ_X.norm (... ...))]]]
-             [(C . args) ▶ ; no type annotations, must infer instantiation
+             [(C . args) ≫ ; no type annotations, must infer instantiation
               [#:with StructName/ty 
                (set-stx-prop/preserved
                 (⊢ StructName : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))
@@ -677,7 +677,7 @@
   )
 
 (define-typed-syntax match2 #:datum-literals (with ->)
-  [(match2 e with . clauses) ▶
+  [(match2 e with . clauses) ≫
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
    [⊢ [[e ≫ e-] ⇒ : τ_e]]
    [#:with ([(~seq p ...) -> e_body] ...) #'clauses]
@@ -696,7 +696,7 @@
 
 (define-typed-syntax match #:datum-literals (with -> ::)
   ;; e is a tuple
-  [(match e with . clauses) ▶
+  [(match e with . clauses) ≫
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
    [⊢ [[e ≫ e-] ⇒ : τ_e]]
    [#:when (×? #'τ_e)]
@@ -715,7 +715,7 @@
               (let- ([x- (acc z)] ...) e_body-))]
        ⇒ : ty_body]]]
   ;; e is a list
-  [(match e with . clauses) ▶
+  [(match e with . clauses) ≫
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
    [⊢ [[e ≫ e-] ⇒ : τ_e]]
    [#:when (List? #'τ_e)]
@@ -753,7 +753,7 @@
                  (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))]
        ⇒ : (⊔ ty_body ...)]]]
   ;; e is a variant
-  [(match e with . clauses) ▶
+  [(match e with . clauses) ≫
    [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
    [⊢ [[e ≫ e-] ⇒ : τ_e]]
    [#:when (and (not (×? #'τ_e)) (not (List? #'τ_e)))]
@@ -836,7 +836,7 @@
 
 ; all λs have type (?∀ (X ...) (→ τ_in ... τ_out))
 (define-typed-syntax λ #:datum-literals (:)
-  [(λ (x:id ...) body) ⇐ : (~?∀ (X ...) (~ext-stlc:→ τ_in ... τ_out)) ▶
+  [(λ (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 ...]))]
@@ -844,7 +844,7 @@
     ⊢ [[body ≫ body-] ⇐ : τ_out]]
    --------
    [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇐ : _]]]
-  [(λ ([x : τ_x] ...) body) ⇐ : (~?∀ (V ...) (~ext-stlc:→ τ_in ... τ_out)) ▶
+  [(λ ([x : τ_x] ...) body) ⇐ : (~?∀ (V ...) (~ext-stlc:→ τ_in ... τ_out)) ≫
    [#:with [X ...] (compute-tyvars #'(τ_x ...))]
    [([X : #%type ≫ X-] ...) ()
     ⊢ [[τ_x ≫ τ_x-] ⇐ : #%type] ...]
@@ -854,7 +854,7 @@
     ⊢ [[body ≫ body-] ⇐ : τ_out]]
    --------
    [⊢ [[_ ≫ (λ- (x- ...) body-)] ⇐ : _]]]
-  [(λ ([x : τ_x] ...) body) ▶
+  [(λ ([x : τ_x] ...) body) ≫
    [#:with [X ...] (compute-tyvars #'(τ_x ...))]
    ;; TODO is there a way to have λs that refer to ids defined after them?
    [([X : #%type ≫ X-] ...) ([x : τ_x ≫ x-] ...)
@@ -868,7 +868,7 @@
 
 ;; #%app --------------------------------------------------
 (define-typed-syntax mlish:#%app #:export-as #%app
-  [(_ e_fn . e_args) ▶
+  [(_ e_fn . e_args) ≫
    ;; compute fn type (ie ∀ and →)
    [⊢ [[e_fn ≫ e_fn-] ⇒ : (~?∀ Xs (~ext-stlc:→ . tyX_args))]]
    ;; solve for type variables Xs
@@ -905,26 +905,26 @@
   [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
                test)
           b ... body] ...+)
-   ⇐ : τ_expected ▶
+   ⇐ : τ_expected ≫
    [⊢ [[test ≫ test-] ⇐ : Bool] ...]
    [⊢ [[(begin b ... body) ≫ body-] ⇐ : τ_expected] ...]
    --------
    [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇐ : _]]]
   [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
                test)
-          b ... body] ...+) ▶
+          b ... body] ...+) ≫
    [⊢ [[test ≫ test-] ⇐ : Bool] ...]
    [⊢ [[(begin b ... body) ≫ body-] ⇒ : τ_body] ...]
    --------
    [⊢ [[_ ≫ (cond- [test- body-] ...)] ⇒ : (⊔ τ_body ...)]]])
 (define-typed-syntax when
-  [(when test body ...) ▶
+  [(when test body ...) ≫
    [⊢ [[test ≫ test-] ⇒ : _]]
    [⊢ [[body ≫ body-] ⇒ : _] ...]
    --------
    [⊢ [[_ ≫ (when- test- body- ... (void-))] ⇒ : Unit]]])
 (define-typed-syntax unless
-  [(unless test body ...) ▶
+  [(unless test body ...) ≫
    [⊢ [[test ≫ test-] ⇒ : _]]
    [⊢ [[body ≫ body-] ⇒ : _] ...]
    --------
@@ -934,21 +934,21 @@
 (define-type-constructor Channel)
 
 (define-typed-syntax make-channel
-  [(make-channel (~and tys {ty})) ▶
+  [(make-channel (~and tys {ty})) ≫
    [#:when (brace? #'tys)]
    --------
    [⊢ [[_ ≫ (make-channel-)] ⇒ : (Channel ty)]]])
 (define-typed-syntax channel-get
-  [(channel-get c) ⇐ : ty ▶
+  [(channel-get c) ⇐ : ty ≫
    [⊢ [[c ≫ c-] ⇐ : (Channel ty)]]
    --------
    [⊢ [[_ ≫ (channel-get- c-)] ⇐ : _]]]
-  [(channel-get c) ▶
+  [(channel-get c) ≫
    [⊢ [[c ≫ c-] ⇒ : (~Channel ty)]]
    --------
    [⊢ [[_ ≫ (channel-get- c-)] ⇒ : ty]]])
 (define-typed-syntax channel-put
-  [(channel-put c v) ▶
+  [(channel-put c v) ≫
    [⊢ [[c ≫ c-] ⇒ : (~Channel ty)]]
    [⊢ [[v ≫ v-] ⇐ : ty]]
    --------
@@ -958,7 +958,7 @@
 
 ;; threads
 (define-typed-syntax thread
-  [(thread th) ▶
+  [(thread th) ≫
    [⊢ [[th ≫ th-] ⇒ : (~?∀ () (~ext-stlc:→ τ_out))]]
    --------
    [⊢ [[_ ≫ (thread- th-)] ⇒ : Thread]]])
@@ -969,13 +969,13 @@
 (define-primop string->number : (→ String Int))
 ;(define-primop number->string : (→ Int String))
 (define-typed-syntax number->string
-  [number->string:id ▶
+  [number->string:id ≫
    --------
    [⊢ [[_ ≫ number->string-] ⇒ : (→ Int String)]]]
-  [(number->string n) ▶
+  [(number->string n) ≫
    --------
    [_ ≻ (number->string n (ext-stlc:#%datum . 10))]]
-  [(number->string n rad) ▶
+  [(number->string n rad) ≫
    [⊢ [[n ≫ n-] ⇐ : Int]]
    [⊢ [[rad ≫ rad-] ⇐ : Int]]
    --------
@@ -986,7 +986,7 @@
 (define-primop string<=? : (→ String String Bool))
 
 (define-typed-syntax string-append
-  [(string-append str ...) ▶
+  [(string-append str ...) ≫
    [⊢ [[str ≫ str-] ⇐ : String] ...]
    --------
    [⊢ [[_ ≫ (string-append- str- ...)] ⇒ : String]]])
@@ -995,54 +995,54 @@
 (define-type-constructor Vector)
 
 (define-typed-syntax vector
-  [(vector (~and tys {ty})) ▶
+  [(vector (~and tys {ty})) ≫
    [#:when (brace? #'tys)]
    --------
    [⊢ [[_ ≫ (vector-)] ⇒ : (Vector ty)]]]
-  [(vector v ...) ⇐ : (Vector ty) ▶
+  [(vector v ...) ⇐ : (Vector ty) ≫
    [⊢ [[v ≫ v-] ⇐ : ty] ...]
    --------
    [⊢ [[_ ≫ (vector- v- ...)] ⇐ : _]]]
-  [(vector v ...) ▶
+  [(vector v ...) ≫
    [⊢ [[v ≫ v-] ⇒ : ty] ...]
    [#:when (same-types? #'(ty ...))]
    [#:with one-ty (stx-car #'(ty ...))]
    --------
    [⊢ [[_ ≫ (vector- v- ...)] ⇒ : (Vector one-ty)]]])
 (define-typed-syntax make-vector
-  [(make-vector n) ▶
+  [(make-vector n) ≫
    --------
    [_ ≻ (make-vector n (ext-stlc:#%datum . 0))]]
-  [(make-vector n e) ▶
+  [(make-vector n e) ≫
    [⊢ [[n ≫ n-] ⇐ : Int]]
    [⊢ [[e ≫ e-] ⇒ : ty]]
    --------
    [⊢ [[_ ≫ (make-vector- n- e-)] ⇒ : (Vector ty)]]])
 (define-typed-syntax vector-length
-  [(vector-length e) ▶
+  [(vector-length e) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Vector _)]]
    --------
    [⊢ [[_ ≫ (vector-length- e-)] ⇒ : Int]]])
 (define-typed-syntax vector-ref
-  [(vector-ref e n) ⇐ : ty ▶
+  [(vector-ref e n) ⇐ : ty ≫
    [⊢ [[e ≫ e-] ⇐ : (Vector ty)]]
    [⊢ [[n ≫ n-] ⇐ : Int]]
    --------
    [⊢ [[_ ≫ (vector-ref- e- n-)] ⇐ : _]]]
-  [(vector-ref e n) ▶
+  [(vector-ref e n) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Vector ty)]]
    [⊢ [[n ≫ n-] ⇐ : Int]]
    --------
    [⊢ [[_ ≫ (vector-ref- e- n-)] ⇒ : ty]]])
 (define-typed-syntax vector-set!
-  [(vector-set! e n v) ▶
+  [(vector-set! e n v) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Vector ty)]]
    [⊢ [[n ≫ n-] ⇐ : Int]]
    [⊢ [[v ≫ v-] ⇐ : ty]]
    --------
    [⊢ [[_ ≫ (vector-set!- e- n- v-)] ⇒ : Unit]]])
 (define-typed-syntax vector-copy!
-  [(vector-copy! dest start src) ▶
+  [(vector-copy! dest start src) ≫
    [⊢ [[dest ≫ dest-] ⇒ : (~Vector ty)]]
    [⊢ [[start ≫ start-] ⇐ : Int]]
    [⊢ [[src ≫ src-] ⇐ : (Vector ty)]]
@@ -1055,13 +1055,13 @@
 (define-type-constructor Sequence)
 
 (define-typed-syntax in-range
-  [(in-range end) ▶
+  [(in-range end) ≫
    --------
    [_ ≻ (in-range (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))]]
-  [(in-range start end) ▶
+  [(in-range start end) ≫
    --------
    [_ ≻ (in-range start end (ext-stlc:#%datum . 1))]]
-  [(in-range start end step) ▶
+  [(in-range start end step) ≫
    [⊢ [[start ≫ start-] ⇐ : Int]]
    [⊢ [[end ≫ end-] ⇐ : Int]]
    [⊢ [[step ≫ step-] ⇐ : Int]]
@@ -1069,42 +1069,42 @@
    [⊢ [[_ ≫ (in-range- start- end- step-)] ⇒ : (Sequence Int)]]])
 
 (define-typed-syntax in-naturals
- [(in-naturals) ▶
+ [(in-naturals) ≫
   --------
   [_ ≻ (in-naturals (ext-stlc:#%datum . 0))]]
- [(in-naturals start) ▶
+ [(in-naturals start) ≫
   [⊢ [[start ≫ start-] ⇐ : Int]]
   --------
   [⊢ [[_ ≫ (in-naturals- start-)] ⇒ : (Sequence Int)]]])
 
 
 (define-typed-syntax in-vector
-  [(in-vector e) ▶
+  [(in-vector e) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Vector ty)]]
    --------
    [⊢ [[_ ≫ (in-vector- e-)] ⇒ : (Sequence ty)]]])
 
 (define-typed-syntax in-list
-  [(in-list e) ▶
+  [(in-list e) ≫
    [⊢ [[e ≫ e-] ⇒ : (~List ty)]]
    --------
    [⊢ [[_ ≫ (in-list- e-)] ⇒ : (Sequence ty)]]])
 
 (define-typed-syntax in-lines
-  [(in-lines e) ▶
+  [(in-lines e) ≫
    [⊢ [[e ≫ e-] ⇐ : String]]
    --------
    [⊢ [[_ ≫ (in-lines- (open-input-string- e-))] ⇒ : (Sequence String)]]])
 
 (define-typed-syntax for
-  [(for ([x:id e]...) b ... body) ▶
+  [(for ([x:id e]...) b ... body) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...)
     ⊢ [[b ≫ b-] ⇒ : _] ... [[body ≫ body-] ⇒ : _]]
    --------
    [⊢ [[_ ≫ (for- ([x- e-] ...) b- ... body-)] ⇒ : Unit]]])
 (define-typed-syntax for*
-  [(for* ([x:id e]...) b ... body) ▶
+  [(for* ([x:id e]...) b ... body) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...)
     ⊢ [[b ≫ b-] ⇒ : _] ... [[body ≫ body-] ⇒ : _]]
@@ -1112,38 +1112,38 @@
    [⊢ [[_ ≫ (for*- ([x- e-] ...) b- ... body-)] ⇒ : Unit]]])
 
 (define-typed-syntax for/list
-  [(for/list ([x:id e]...) body) ▶
+  [(for/list ([x:id e]...) body) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
    --------
    [⊢ [[_ ≫ (for/list- ([x- e-] ...) body-)] ⇒ : (List ty_body)]]])
 (define-typed-syntax for/vector
-  [(for/vector ([x:id e]...) body) ▶
+  [(for/vector ([x:id e]...) body) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
    --------
    [⊢ [[_ ≫ (for/vector- ([x- e-] ...) body-)] ⇒ : (Vector ty_body)]]])
 (define-typed-syntax for*/vector
-  [(for*/vector ([x:id e]...) body) ▶
+  [(for*/vector ([x:id e]...) body) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
    --------
    [⊢ [[_ ≫ (for*/vector- ([x- e-] ...) body-)] ⇒ : (Vector ty_body)]]])
 (define-typed-syntax for*/list
-  [(for*/list ([x:id e]...) body) ▶
+  [(for*/list ([x:id e]...) body) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : ty_body]]
    --------
    [⊢ [[_ ≫ (for*/list- ([x- e-] ...) body-)] ⇒ : (List ty_body)]]])
 (define-typed-syntax for/fold
-  [(for/fold ([acc init]) ([x:id e] ...) body) ⇐ : τ_expected ▶
+  [(for/fold ([acc init]) ([x:id e] ...) body) ⇐ : τ_expected ≫
    [⊢ [[init ≫ init-] ⇐ : τ_expected]]
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([acc : τ_expected ≫ acc-] [x : ty ≫ x-] ...)
     ⊢ [[body ≫ body-] ⇐ : τ_expected]]
    --------
    [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇐ : _]]]
-  [(for/fold ([acc init]) ([x:id e] ...) body) ▶
+  [(for/fold ([acc init]) ([x:id e] ...) body) ≫
    [⊢ [[init ≫ init-] ⇒ : τ_init]]
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([acc : τ_init ≫ acc-] [x : ty ≫ x-] ...)
@@ -1152,7 +1152,7 @@
    [⊢ [[_ ≫ (for/fold- ([acc- init-]) ([x- e-] ...) body-)] ⇒ : τ_init]]])
 
 (define-typed-syntax for/hash
-  [(for/hash ([x:id e]...) body) ▶
+  [(for/hash ([x:id e]...) body) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...) ⊢ [[body ≫ body-] ⇒ : (~× ty_k ty_v)]]
    --------
@@ -1164,7 +1164,7 @@
 (define-typed-syntax for/sum
   [(for/sum ([x:id e]... 
              (~optional (~seq #:when guard) #:defaults ([guard #'#t])))
-     body) ▶
+     body) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Sequence ty)] ...]
    [() ([x : ty ≫ x-] ...)
     ⊢ [[guard ≫ guard-] ⇒ : _] [[body ≫ body-] ⇐ : Int]]
@@ -1173,41 +1173,41 @@
 
 ; printing and displaying
 (define-typed-syntax printf
-  [(printf str e ...) ▶
+  [(printf str e ...) ≫
    [⊢ [[str ≫ s-] ⇐ : String]]
    [⊢ [[e ≫ e-] ⇒ : ty] ...]
    --------
    [⊢ [[_ ≫ (printf- s- e- ...)] ⇒ : Unit]]])
 (define-typed-syntax format
-  [(format str e ...) ▶
+  [(format str e ...) ≫
    [⊢ [[str ≫ s-] ⇐ : String]]
    [⊢ [[e ≫ e-] ⇒ : ty] ...]
    --------
    [⊢ [[_ ≫ (format- s- e- ...)] ⇒ : String]]])
 (define-typed-syntax display
-  [(display e) ▶
+  [(display e) ≫
    [⊢ [[e ≫ e-] ⇒ : _]]
    --------
    [⊢ [[_ ≫ (display- e-)] ⇒ : Unit]]])
 (define-typed-syntax displayln
-  [(displayln e) ▶
+  [(displayln e) ≫
    [⊢ [[e ≫ e-] ⇒ : _]]
    --------
    [⊢ [[_ ≫ (displayln- e-)] ⇒ : Unit]]])
 (define-primop newline : (→ Unit))
 
 (define-typed-syntax list->vector
-  [(list->vector e) ⇐ : (~Vector ty) ▶
+  [(list->vector e) ⇐ : (~Vector ty) ≫
    [⊢ [[e ≫ e-] ⇐ : (List ty)]]
    --------
    [⊢ [[_ ≫ (list->vector- e-)] ⇐ : _]]]
-  [(list->vector e) ▶
+  [(list->vector e) ≫
    [⊢ [[e ≫ e-] ⇒ : (~List ty)]]
    --------
    [⊢ [[_ ≫ (list->vector- e-)] ⇒ : (Vector ty)]]])
 
 (define-typed-syntax let
-  [(let name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body) ▶
+  [(let name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body) ≫
    [⊢ [[e ≫ e-] ⇒ : ty_e] ...]
    [() ([name : (→ ty_e ... ty.norm) ≫ name-] [x : ty_e ≫ x-] ...)
     ⊢ [[b ≫ b-] ⇒ : _] ... [[body ≫ body-] ⇐ : ty.norm]]
@@ -1215,21 +1215,21 @@
    [⊢ [[_ ≫ (letrec- ([name- (λ- (x- ...) b- ... body-)])
               (name- e- ...))]
        ⇒ : ty.norm]]]
-  [(let ([x:id e] ...) body ...) ▶
+  [(let ([x:id e] ...) body ...) ≫
    --------
    [_ ≻ (ext-stlc:let ([x e] ...) (begin body ...))]])
 (define-typed-syntax let*
-  [(let* ([x:id e] ...) body ...) ▶
+  [(let* ([x:id e] ...) body ...) ≫
    --------
    [_ ≻ (ext-stlc:let* ([x e] ...) (begin body ...))]])
 
 (define-typed-syntax begin
-  [(begin body ... b) ⇐ : τ_expected ▶
+  [(begin body ... b) ⇐ : τ_expected ≫
    [⊢ [[body ≫ body-] ⇒ : _] ...]
    [⊢ [[b ≫ b-] ⇐ : τ_expected]]
    --------
    [⊢ [[_ ≫ (begin- body- ... b-)] ⇐ : _]]]
-  [(begin body ... b) ▶
+  [(begin body ... b) ≫
    [⊢ [[body ≫ body-] ⇒ : _] ...]
    [⊢ [[b ≫ b-] ⇒ : τ]]
    --------
@@ -1239,18 +1239,18 @@
 (define-type-constructor Hash #:arity = 2)
 
 (define-typed-syntax in-hash
-  [(in-hash e) ▶
+  [(in-hash e) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Hash ty_k ty_v)]]
    --------
    [⊢ [[_ ≫ (hash-map- e- list-)] ⇒ : (Sequence (stlc+rec-iso:× ty_k ty_v))]]])
 
 ; mutable hashes
 (define-typed-syntax hash
-  [(hash (~and tys {ty_key ty_val})) ▶
+  [(hash (~and tys {ty_key ty_val})) ≫
    [#:when (brace? #'tys)]
    --------
    [⊢ [[_ ≫ (make-hash-)] ⇒ : (Hash ty_key ty_val)]]]
-  [(hash (~seq k v) ...) ▶
+  [(hash (~seq k v) ...) ≫
    [⊢ [[k ≫ k-] ⇒ : ty_k] ...]
    [⊢ [[v ≫ v-] ⇒ : ty_v] ...]
    [#:when (same-types? #'(ty_k ...))]
@@ -1260,33 +1260,33 @@
    --------
    [⊢ [[_ ≫ (make-hash- (list- (cons- k- v-) ...))] ⇒ : (Hash ty_key ty_val)]]])
 (define-typed-syntax hash-set!
-  [(hash-set! h k v) ▶
+  [(hash-set! h k v) ≫
    [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k ty_v)]]
    [⊢ [[k ≫ k-] ⇐ : ty_k]]
    [⊢ [[v ≫ v-] ⇐ : ty_v]]
    --------
    [⊢ [[_ ≫ (hash-set!- h- k- v-)] ⇒ : Unit]]])
 (define-typed-syntax hash-ref
-  [(hash-ref h k) ▶
+  [(hash-ref h k) ≫
    [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k ty_v)]]
    [⊢ [[k ≫ k-] ⇐ : ty_k]]
    --------
    [⊢ [[_ ≫ (hash-ref- h- k-)] ⇒ : ty_v]]]
-  [(hash-ref h k fail) ▶
+  [(hash-ref h k fail) ≫
    [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k ty_v)]]
    [⊢ [[k ≫ k-] ⇐ : ty_k]]
    [⊢ [[fail ≫ fail-] ⇐ : (→ ty_v)]]
    --------
    [⊢ [[_ ≫ (hash-ref- h- k- fail-)] ⇒ : ty_val]]])
 (define-typed-syntax hash-has-key?
-  [(hash-has-key? h k) ▶
+  [(hash-has-key? h k) ≫
    [⊢ [[h ≫ h-] ⇒ : (~Hash ty_k _)]]
    [⊢ [[k ≫ k-] ⇐ : ty_k]]
    --------
    [⊢ [[_ ≫ (hash-has-key?- h- k-)] ⇒ : Bool]]])
 
 (define-typed-syntax hash-count
-  [(hash-count h) ▶
+  [(hash-count h) ≫
    [⊢ [[h ≫ h-] ⇒ : (~Hash _ _)]]
    --------
    [⊢ [[_ ≫ (hash-count- h-)] ⇒ : Int]]])
@@ -1298,10 +1298,10 @@
 (define-primop string-upcase : (→ String String))
 
 (define-typed-syntax write-string
- [(write-string str out) ▶
+ [(write-string str out) ≫
   --------
   [_ ≻ (write-string str out (ext-stlc:#%datum . 0) (string-length str))]]
- [(write-string str out start end) ▶
+ [(write-string str out start end) ≫
   [⊢ [[str ≫ str-] ⇐ : String]]
   [⊢ [[out ≫ out-] ⇐ : String-Port]]
   [⊢ [[start ≫ start-] ⇐ : Int]]
@@ -1310,7 +1310,7 @@
   [⊢ [[_ ≫ (begin- (write-string- str- out- start- end-) (void-))] ⇒ : Unit]]])
 
 (define-typed-syntax string-length
- [(string-length str) ▶
+ [(string-length str) ≫
   [⊢ [[str ≫ str-] ⇐ : String]]
   --------
   [⊢ [[_ ≫ (string-length- str-)] ⇒ : Int]]])
@@ -1318,11 +1318,11 @@
 (define-primop string-set! : (→ String Int Char Unit))
 (define-primop string-ref : (→ String Int Char))
 (define-typed-syntax string-copy!
-  [(string-copy! dest dest-start src) ▶
+  [(string-copy! dest dest-start src) ≫
    --------
    [_ ≻ (string-copy!
          dest dest-start src (ext-stlc:#%datum . 0) (string-length src))]]
-  [(string-copy! dest dest-start src src-start src-end) ▶
+  [(string-copy! dest dest-start src src-start src-end) ≫
    [⊢ [[dest ≫ dest-] ⇐ : String]]
    [⊢ [[src ≫ src-] ⇐ : String]]
    [⊢ [[dest-start ≫ dest-start-] ⇐ : Int]]
@@ -1343,7 +1343,7 @@
 (define-primop real->decimal-string : (→ Float Int String))
 (define-primop fx->fl : (→ Int Float))
 (define-typed-syntax quotient+remainder
-  [(quotient+remainder x y) ▶
+  [(quotient+remainder x y) ≫
    [⊢ [[x ≫ x-] ⇐ : Int]]
    [⊢ [[y ≫ y-] ⇐ : Int]]
    --------
@@ -1353,19 +1353,19 @@
 (define-primop quotient : (→ Int Int Int))
 
 (define-typed-syntax set!
-  [(set! x:id e) ▶
+  [(set! x:id e) ≫
    [⊢ [[x ≫ x-] ⇒ : ty_x]]
    [⊢ [[e ≫ e-] ⇐ : ty_x]]
    --------
    [⊢ [[_ ≫ (set!- x e-)] ⇒ : Unit]]])
 
 (define-typed-syntax provide-type
-  [(provide-type ty ...) ▶
+  [(provide-type ty ...) ≫
    --------
    [_ ≻ (provide- ty ...)]])
 
 (define-typed-syntax provide
-  [(provide x:id ...) ▶
+  [(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 ...))]
@@ -1375,7 +1375,7 @@
           (stlc+rec-iso:define-type-alias x-ty ty_x) ...
           (provide- x-ty ...))]])
 (define-typed-syntax require-typed
-  [(require-typed x:id ... #:from mod) ▶
+  [(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 ...))]
    --------
@@ -1388,14 +1388,14 @@
 (define-primop regexp : (→ String Regexp))
 
 (define-typed-syntax equal?
-  [(equal? e1 e2) ▶
+  [(equal? e1 e2) ≫
    [⊢ [[e1 ≫ e1-] ⇒ : ty1]]
    [⊢ [[e2 ≫ e2-] ⇐ : ty1]]
    --------
    [⊢ [[_ ≫ (equal?- e1- e2-)] ⇒ : Bool]]])
 
 (define-typed-syntax read-int
-  [(read-int) ▶
+  [(read-int) ≫
    --------
    [⊢ [[_ ≫ (let- ([x (read-)])
               (cond- [(exact-integer?- x) x]
diff --git a/tapl/typed-lang-builder/stlc+box.rkt b/tapl/typed-lang-builder/stlc+box.rkt
index e3a9d24..d0ac8d7 100644
--- a/tapl/typed-lang-builder/stlc+box.rkt
+++ b/tapl/typed-lang-builder/stlc+box.rkt
@@ -12,19 +12,19 @@
 (define-type-constructor Ref)
 
 (define-typed-syntax ref
-  [(ref e) ▶
+  [(ref e) ≫
    [⊢ [[e ≫ e-] ⇒ : τ]]
    --------
    [⊢ [[_ ≫ (box- e-)] ⇒ : (Ref τ)]]])
 
 (define-typed-syntax deref
-  [(deref e) ▶
+  [(deref e) ≫
    [⊢ [[e ≫ e-] ⇒ : (~Ref τ)]]
    --------
    [⊢ [[_ ≫ (unbox- e-)] ⇒ : τ]]])
 
 (define-typed-syntax := #:literals (:=)
-  [(:= e_ref e) ▶
+  [(:= e_ref e) ≫
    [⊢ [[e_ref ≫ e_ref-] ⇒ : (~Ref τ)]]
    [⊢ [[e ≫ e-] ⇐ : τ]]
    --------
diff --git a/tapl/typed-lang-builder/stlc+cons.rkt b/tapl/typed-lang-builder/stlc+cons.rkt
index 65a52c5..39344d7 100644
--- a/tapl/typed-lang-builder/stlc+cons.rkt
+++ b/tapl/typed-lang-builder/stlc+cons.rkt
@@ -13,68 +13,68 @@
 (define-type-constructor List)
 
 (define-typed-syntax nil
-  [(nil ~! τi:type-ann) ▶
+  [(nil ~! τi:type-ann) ≫
    --------
    [⊢ [[_ ≫ null-] ⇒ : (List τi.norm)]]]
   ; minimal type inference
-  [nil:id ⇐ : (~List τ) ▶
+  [nil:id ⇐ : (~List τ) ≫
    --------
    [⊢ [[_ ≫ null-] ⇐ : _]]])
 (define-typed-syntax cons
-  [(cons e1 e2) ▶
+  [(cons e1 e2) ≫
    [⊢ [[e1 ≫ e1-] ⇒ : τ1]]
    [⊢ [[e2 ≫ e2-] ⇐ : (List τ1)]]
    --------
    [⊢ [[_ ≫ (cons- e1- e2-)] ⇒ : (List τ1)]]])
 (define-typed-syntax isnil
-  [(isnil e) ▶
+  [(isnil e) ≫
    [⊢ [[e ≫ e-] ⇒ : (~List _)]]
    --------
    [⊢ [[_ ≫ (null?- e-)] ⇒ : Bool]]])
 (define-typed-syntax head
-  [(head e) ▶
+  [(head e) ≫
    [⊢ [[e ≫ e-] ⇒ : (~List τ)]]
    --------
    [⊢ [[_ ≫ (car- e-)] ⇒ : τ]]])
 (define-typed-syntax tail
-  [(tail e) ▶
+  [(tail e) ≫
    [⊢ [[e ≫ e-] ⇒ : τ-lst]]
    [#:fail-unless (List? #'τ-lst)
     (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
    --------
    [⊢ [[_ ≫ (cdr- e-)] ⇒ : τ-lst]]])
 (define-typed-syntax list
-  [(list) ▶
+  [(list) ≫
    --------
    [_ ≻ nil]]
-  [(list x . rst) ⇐ : (~List τ) ▶ ; has expected type
+  [(list x . rst) ⇐ : (~List τ) ≫ ; has expected type
    --------
    [⊢ [[_ ≫ (cons (add-expected x τ) (list . rst))] ⇐ : _]]]
-  [(list x . rst) ▶ ; no expected type
+  [(list x . rst) ≫ ; no expected type
    --------
    [_ ≻ (cons x (list . rst))]])
 (define-typed-syntax reverse
-  [(reverse e) ▶
+  [(reverse e) ≫
    [⊢ [[e ≫ e-] ⇒ : τ-lst]]
    [#:fail-unless (List? #'τ-lst)
     (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
    --------
    [⊢ [[_ ≫ (reverse- e-)] ⇒ : τ-lst]]])
 (define-typed-syntax length
-  [(length e) ▶
+  [(length e) ≫
    [⊢ [[e ≫ e-] ⇒ : τ-lst]]
    [#:fail-unless (List? #'τ-lst)
     (format "Expected a list type, got: ~a" (type->str #'τ-lst))]
    --------
    [⊢ [[_ ≫ (length- e-)] ⇒ : Int]]])
 (define-typed-syntax list-ref
-  [(list-ref e n) ▶
+  [(list-ref e n) ≫
    [⊢ [[e ≫ e-] ⇒ : (~List τ)]]
    [⊢ [[n ≫ n-] ⇐ : Int]]
    --------
    [⊢ [[_ ≫ (list-ref- e- n-)] ⇒ : τ]]])
 (define-typed-syntax member
-  [(member v e) ▶
+  [(member v e) ≫
    [⊢ [[e ≫ e-] ⇒ : (~List τ)]]
    [⊢ [[v ≫ v-] ⇐ : τ]]
    --------
diff --git a/tapl/typed-lang-builder/stlc+effect.rkt b/tapl/typed-lang-builder/stlc+effect.rkt
index 8b2485b..620128e 100644
--- a/tapl/typed-lang-builder/stlc+effect.rkt
+++ b/tapl/typed-lang-builder/stlc+effect.rkt
@@ -29,7 +29,7 @@
 
 
 (define-typed-syntax effect:#%app #:export-as #%app
-  [(_ efn e ...) ▶
+  [(_ efn e ...) ≫
    [⊢ [[efn ≫ e_fn-]
        (⇒ : (~→ τ_in ... τ_out)
           (⇒ ν (~locs tyns ...))
@@ -54,7 +54,7 @@
        (⇒ ! (locs fds ... tyds ... ds ... ...))]]])
 
 (define-typed-syntax λ
-  [(λ bvs:type-ctx e) ▶
+  [(λ bvs:type-ctx e) ≫
    [() ([bvs.x : bvs.type ≫ x-] ...) ⊢
        [[e ≫ e-]
         (⇒ : τ_res)
@@ -71,7 +71,7 @@
 (define-type-constructor Ref)
 
 (define-typed-syntax ref
-  [(ref e) ▶
+  [(ref e) ≫
    [⊢ [[e ≫ e-]
        (⇒ : τ)
        (⇒ ν (~locs ns ...))
@@ -84,7 +84,7 @@
        (⇒ := (locs as ...))
        (⇒ ! (locs ds ...))]]])
 (define-typed-syntax deref
-  [(deref e) ▶
+  [(deref e) ≫
    [⊢ [[e ≫ e-]
        (⇒ : (~Ref ty))
        (⇒ ν (~locs ns ...))
@@ -97,7 +97,7 @@
        (⇒ := (locs as ...))
        (⇒ ! (locs #,(syntax-position stx) ds ...))]]])
 (define-typed-syntax := #:literals (:=)
-  [(:= e_ref e) ▶
+  [(:= e_ref e) ≫
    [⊢ [[e_ref ≫ e_ref-]
        (⇒ : (~Ref ty))
        (⇒ ν (~locs ns1 ...))
diff --git a/tapl/typed-lang-builder/stlc+lit.rkt b/tapl/typed-lang-builder/stlc+lit.rkt
index 15fc420..d470462 100644
--- a/tapl/typed-lang-builder/stlc+lit.rkt
+++ b/tapl/typed-lang-builder/stlc+lit.rkt
@@ -32,9 +32,9 @@
 (define-primop + : (→ Int Int Int))
 
 (define-typed-syntax #%datum
-  [(#%datum . n:integer) ▶
+  [(#%datum . n:integer) ≫
    --------
    [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Int]]]
-  [(_ . x) ▶
+  [(_ . x) ≫
    --------
    [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
diff --git a/tapl/typed-lang-builder/stlc+rec-iso.rkt b/tapl/typed-lang-builder/stlc+rec-iso.rkt
index c0ebad5..a673ddd 100644
--- a/tapl/typed-lang-builder/stlc+rec-iso.rkt
+++ b/tapl/typed-lang-builder/stlc+rec-iso.rkt
@@ -37,13 +37,13 @@
   (current-typecheck-relation type=?))
 
 (define-typed-syntax unfld
-  [(unfld τ:type-ann e) ▶
+  [(unfld τ:type-ann e) ≫
    [#:with (~μ* (tv) τ_body) #'τ.norm]
    [⊢ [[e ≫ e-] ⇐ : τ.norm]]
    --------
    [⊢ [[_ ≫ e-] ⇒ : #,(subst #'τ.norm #'tv #'τ_body)]]])
 (define-typed-syntax fld
-  [(fld τ:type-ann e) ▶
+  [(fld τ:type-ann e) ≫
    [#:with (~μ* (tv) τ_body) #'τ.norm]
    [#:with τ_e (subst #'τ.norm #'tv #'τ_body)]
    [⊢ [[e ≫ e-] ⇐ : τ_e]]
diff --git a/tapl/typed-lang-builder/stlc+reco+sub.rkt b/tapl/typed-lang-builder/stlc+reco+sub.rkt
index 64032ca..77bc910 100644
--- a/tapl/typed-lang-builder/stlc+reco+sub.rkt
+++ b/tapl/typed-lang-builder/stlc+reco+sub.rkt
@@ -14,10 +14,10 @@
 ;; - records and variants from stlc+reco+var
 
 (define-typed-syntax #%datum
-  [(#%datum . n:number) ▶
+  [(#%datum . n:number) ≫
    --------
    [_ ≻ (stlc+sub:#%datum . n)]]
-  [(#%datum . x) ▶
+  [(#%datum . x) ≫
    --------
    [_ ≻ (stlc+reco+var:#%datum . x)]])
 
diff --git a/tapl/typed-lang-builder/stlc+reco+var.rkt b/tapl/typed-lang-builder/stlc+reco+var.rkt
index eb894d9..2257546 100644
--- a/tapl/typed-lang-builder/stlc+reco+var.rkt
+++ b/tapl/typed-lang-builder/stlc+reco+var.rkt
@@ -28,7 +28,7 @@
            [(_ x ...) #'ty]))]))
 
 (define-typed-syntax define
-  [(define x:id : τ:type e:expr) ▶
+  [(define x:id : τ:type e:expr) ≫
    ;This wouldn't work with mutually recursive definitions
    ;[⊢ [[e ≫ e-] ⇐ τ.norm]]
    ;So expand to an ann form instead.
@@ -36,7 +36,7 @@
    [_ ≻ (begin-
           (define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
           (define- y (ann e : τ.norm)))]]
-  [(define x:id e) ▶
+  [(define x:id e) ≫
    [⊢ [[e ≫ e-] ⇒ : τ]]
    [#:with y (generate-temporary #'x)]
    --------
@@ -87,12 +87,12 @@
 
 ;; records
 (define-typed-syntax tup #:datum-literals (=)
-  [(tup [l:id = e] ...) ▶
+  [(tup [l:id = e] ...) ≫
    [⊢ [[e ≫ e-] ⇒ : τ] ...]
    --------
    [⊢ [[_ ≫ (list- (list- 'l e-) ...)] ⇒ : (× [l : τ] ...)]]])
 (define-typed-syntax proj #:literals (quote)
-  [(proj e_rec l:id) ▶
+  [(proj e_rec l:id) ≫
    [⊢ [[e_rec ≫ e_rec-] ⇒ : τ_e]]
    [#:fail-unless (×? #'τ_e)
     (format "Expected expression ~s to have × type, got: ~a"
@@ -145,10 +145,10 @@
        (add-orig res (get-orig res))])))
 
 (define-typed-syntax var #:datum-literals (as =)
-  [(var l:id = e as τ:type) ▶
+  [(var l:id = e as τ:type) ≫
    --------
    [_ ≻ (ann (var l = e) : τ.norm)]]
-  [(var l:id = e) ⇐ : τ ▶
+  [(var l:id = e) ⇐ : τ ≫
    [#:fail-unless (∨? #'τ)
     (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ))]
    [#:with τ_e
@@ -162,7 +162,7 @@
 
 (define-typed-syntax case
   #:datum-literals (of =>)
-  [(case e [l:id x:id => e_l] ...) ▶
+  [(case e [l:id x:id => e_l] ...) ≫
    [#: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"]
diff --git a/tapl/typed-lang-builder/stlc+sub.rkt b/tapl/typed-lang-builder/stlc+sub.rkt
index 64121ec..5c3906f 100644
--- a/tapl/typed-lang-builder/stlc+sub.rkt
+++ b/tapl/typed-lang-builder/stlc+sub.rkt
@@ -28,16 +28,16 @@
 (define-primop * : (→ Num Num Num))
 
 (define-typed-syntax #%datum
-  [(#%datum . n:nat) ▶
+  [(#%datum . n:nat) ≫
    --------
    [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Nat]]]
-  [(#%datum . n:integer) ▶
+  [(#%datum . n:integer) ≫
    --------
    [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Int]]]
-  [(#%datum . n:number) ▶
+  [(#%datum . n:number) ≫
    --------
    [⊢ [[_ ≫ (#%datum- . n)] ⇒ : Num]]]
-  [(#%datum . x) ▶
+  [(#%datum . x) ≫
    --------
    [_ ≻ (ext:#%datum . x)]])
 
diff --git a/tapl/typed-lang-builder/stlc+tup.rkt b/tapl/typed-lang-builder/stlc+tup.rkt
index 0201d3e..2ccbe7a 100644
--- a/tapl/typed-lang-builder/stlc+tup.rkt
+++ b/tapl/typed-lang-builder/stlc+tup.rkt
@@ -16,18 +16,18 @@
                     (make-list (stx-length (stx-cdr stx)) covariant)))
 
 (define-typed-syntax tup
-  [(tup e ...) ⇐ : (~× τ ...) ▶
+  [(tup e ...) ⇐ : (~× τ ...) ≫
    [#:when (stx-length=? #'[e ...] #'[τ ...])]
    [⊢ [[e ≫ e-] ⇐ : τ] ...]
    --------
    [⊢ [[_ ≫ (list- e- ...)] ⇐ : _]]]
-  [(tup e ...) ▶
+  [(tup e ...) ≫
    [⊢ [[e ≫ e-] ⇒ : τ] ...]
    --------
    [⊢ [[_ ≫ (list- e- ...)] ⇒ : (× τ ...)]]])
 
 (define-typed-syntax proj
-  [(proj e_tup n:nat) ▶
+  [(proj e_tup n:nat) ≫
    [⊢ [[e_tup ≫ e_tup-] ⇒ : (~× τ ...)]]
    [#:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large"]
    --------
diff --git a/tapl/typed-lang-builder/stlc.rkt b/tapl/typed-lang-builder/stlc.rkt
index 2e05ab9..d3efd01 100644
--- a/tapl/typed-lang-builder/stlc.rkt
+++ b/tapl/typed-lang-builder/stlc.rkt
@@ -28,17 +28,17 @@
                         (list covariant))])))
 
 (define-typed-syntax λ #:datum-literals (:)
-  [(λ ([x:id : τ_in:type] ...) e) ▶
+  [(λ ([x:id : τ_in:type] ...) e) ≫
    [() ([x : τ_in.norm ≫ x-] ...) ⊢ [[e ≫ e-] ⇒ : τ_out]]
    --------
    [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇒ : (→ τ_in.norm ... τ_out)]]]
-  [(λ (x:id ...) e) ⇐ : (~→ τ_in ... τ_out) ▶
+  [(λ (x:id ...) e) ⇐ : (~→ τ_in ... τ_out) ≫
    [() ([x : τ_in ≫ x-] ...) ⊢ [[e ≫ e-] ⇐ : τ_out]]
    --------
    [⊢ [[_ ≫ (λ- (x- ...) e-)] ⇐ : _]]])
 
 (define-typed-syntax #%app
-  [(_ e_fn e_arg ...) ▶
+  [(_ 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 ...])]
@@ -47,7 +47,7 @@
    [⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ : τ_out]]])
 
 (define-typed-syntax ann #:datum-literals (:)
-  [(ann e : τ:type) ▶
+  [(ann e : τ:type) ≫
    [⊢ [[e ≫ e-] ⇐ : τ.norm]]
    --------
    [⊢ [[_ ≫ e-] ⇒ : τ.norm]]])
diff --git a/tapl/typed-lang-builder/sysf.rkt b/tapl/typed-lang-builder/sysf.rkt
index 52a68e9..9dbc984 100644
--- a/tapl/typed-lang-builder/sysf.rkt
+++ b/tapl/typed-lang-builder/sysf.rkt
@@ -15,18 +15,18 @@
 (define-type-constructor ∀ #:bvs >= 0)
 
 (define-typed-syntax Λ
-  [(Λ (tv:id ...) e) ▶
+  [(Λ (tv:id ...) e) ≫
    [([tv : #%type ≫ tv-] ...) () ⊢ [[e ≫ e-] ⇒ : τ]]
    --------
    [⊢ [[_ ≫ e-] ⇒ : (∀ (tv- ...) τ)]]])
 
 (define-typed-syntax inst
-  [(inst e τ:type ...) ▶
+  [(inst e τ:type ...) ≫
    [⊢ [[e ≫ e-] ⇒ : (~∀ tvs τ_body)]]
    [#:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)]
    --------
    [⊢ [[_ ≫ e-] ⇒ : τ_inst]]]
-  [(inst e) ▶
+  [(inst e) ≫
    --------
    [_ ≻ e]])
 
diff --git a/tapl/typed-lang-builder/typed-lang-builder.rkt b/tapl/typed-lang-builder/typed-lang-builder.rkt
index e062cc4..885eb27 100644
--- a/tapl/typed-lang-builder/typed-lang-builder.rkt
+++ b/tapl/typed-lang-builder/typed-lang-builder.rkt
@@ -233,8 +233,8 @@
                               (not (typecheck? (typeof b) #'τ)))
                      (raise-⇐-expected-type-error #'left b #'τ (typeof b)))
                    (assign-type b #'τ)))])
-  (define-syntax-class rule #:datum-literals (▶)
-    [pattern [pat:pat ▶
+  (define-syntax-class rule #:datum-literals (≫)
+    [pattern [pat:pat ≫
               clause:clause ...
               :---
               last-clause:last-clause]