diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
index 7ca5aa2..f879795 100644
--- a/turnstile/examples/rosette/bv.rkt
+++ b/turnstile/examples/rosette/bv.rkt
@@ -1,13 +1,12 @@
 #lang turnstile
-(extends "rosette.rkt" #:except bv) ; extends typed rosette
+(extends "rosette.rkt" #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) ; extends typed rosette
 (require (prefix-in ro: rosette)) ; untyped 
-(require (except-in "rosette.rkt" #%app define)) ; typed
+;(require (except-in "rosette.rkt" #%app define)) ; typed
 (require (only-in sdsl/bv/lang/bvops bvredand bvredor)
          (prefix-in bv: (only-in sdsl/bv/lang/bvops BV)))
 (require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form))
 (provide bool->bv thunk)
 
-;(define current-bvpred-internal (ro:make-parameter (ro:bitvector 4)))
 ;; this must be a macro in order to support Racket's overloaded set/get 
 ;; parameter patterns
 (define-typed-syntax current-bvpred
@@ -39,15 +38,10 @@
    --------
    [⊢ [[_ ≫ ((lambda- () (ro:define-symbolic* b e_size-) b))] ⇒ : BV]]])
 
-(define-syntax-rule (bool->bv b) (if b (bv 1) (bv 0)))
-#;(define-typed-syntax bool->bv
-  [(_ e) ≫
-   [⊢ [[e ≫ e-] ⇐ : Bool]]
-   --------
-   [⊢ [[_ ≫ (if- e- (bv 1) (bv 0))] ⇒ : BV]]])
-
-;; (define- (bvredor x)  (ro:bveq (ro:bveq x (bv 0)) (bv 0)))
-;; (define- (bvredand x) (ro:bveq x (bv -1)))
+(define-syntax-rule (bool->bv b) 
+  (rosette:if b 
+              (bv (rosette:#%datum . 1)) 
+              (bv (rosette:#%datum . 0))))
 (define-primop bvredor : (→ BV BV))
 (define-primop bvredand : (→ BV BV))
 
@@ -64,7 +58,7 @@
 (define-typed-syntax define-fragment
   [(_ (id param ...) #:implements spec #:library lib-expr) ≫
    --------
-   [_ ≻ (define-fragment (id param ...) #:implements spec #:library lib-expr #:minbv 4)]]
+   [_ ≻ (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"]
@@ -96,18 +90,4 @@
    --------
    [⊢ [[_ ≫ (bv:bvlib [{id- ...} n-] ...)] ⇒ : Lib]]])
 
-
-#;(define-typed-syntax synthesize-fragment
-  [(_ (id param ...) #:implements spec #:library lib-expr)
-   --------
-   [_ ≻ (synthesize-fragment (id param ...) #:implements spec #:library lib-expr #:minbv 4)]]
-  [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv)
-   [⊢ [[spec ≫ spec-] ⇐ : Spec]]
-   [⊢ [[lib-expr ≫ lib-expr-] ⇐ : Lib]]
-   [⊢ [[minbv ≫ minbv-] ⇐ : Int]]]
-   --------
-   [⊢ [[_ ≫ (bv:synthesize-fragment (id param) #:implements spec- 
-                                                #:library lib-expr- 
-                                                #:minbv minbv-)] ⇒ : BV]])
-
-(define-syntax-rule (thunk e) (λ () e))
+(define-syntax-rule (thunk e) (rosette:λ () e))
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
index 0de8b68..2960189 100644
--- a/turnstile/examples/rosette/rosette.rkt
+++ b/turnstile/examples/rosette/rosette.rkt
@@ -2,8 +2,9 @@
 ;(require (only-in rosette bv bitvector))
 ;(require (only-in rosette [exact-integer? integer?]))
 (extends "../ext-stlc.rkt" #:except if)
+(reuse List #:from "../stlc+cons.rkt")
 (require (prefix-in stlc: (only-in "../stlc+reco+var.rkt" define λ)))
-(require (only-in "../stlc+reco+var.rkt" define-type-alias))
+(require (only-in "../stlc+reco+var.rkt" define-type-alias Int Bool →))
 (require (prefix-in ro: rosette))
 (provide BVPred)
 
@@ -31,6 +32,16 @@
 ;; ----------------------------------------------------------------------------
 ;; Racket stuff
 
+(define-base-type Symbol)
+
+(define-typed-syntax quote
+  [(_ x:id) ≫
+   --------
+   [⊢ [[_ ≫ (quote- x)] ⇒ : Symbol]]]
+  [(_ (x:id ...)) ≫
+   --------
+   [⊢ [[_ ≫ (quote- (x ...))] ⇒ : (stlc+cons:List Symbol)]]])
+
 (define-type-constructor Param #:arity = 1)
 
 (define-rosette-primop boolean? : (→ Bool Bool))
diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt
index 8b0f6fa..40674c8 100644
--- a/turnstile/examples/stlc+lit.rkt
+++ b/turnstile/examples/stlc+lit.rkt
@@ -19,8 +19,8 @@
   (syntax-parser #:datum-literals (:)
     [(define-primop op:id : τ:type)
      #:with op/tc (generate-temporary #'op)
-     #'(begin-
-         (provide- (rename-out- [op/tc op]))
+     #`(begin-
+         (provide- #,(syntax/loc this-syntax (rename-out- [op/tc op])))
          (define-primop op/tc op : τ))]
     [(define-primop op/tc op : τ)
      #'(begin-
diff --git a/turnstile/examples/tests/rosette/bv-tests.rkt b/turnstile/examples/tests/rosette/bv-tests.rkt
index b51cf98..7d87dcf 100644
--- a/turnstile/examples/tests/rosette/bv-tests.rkt
+++ b/turnstile/examples/tests/rosette/bv-tests.rkt
@@ -22,8 +22,8 @@
 (check-type (bool->bv i) : BV -> (bv 1))
 (check-type (bool->bv b) : BV -> (if b (bv 1) (bv 0)))
 
-(check-type (bvredor (bv 1)) : Bool)
-(check-type (bvredand (bv 1)) : Bool)
+(check-type (bvredor (bv 1)) : BV)
+(check-type (bvredand (bv 1)) : BV)
 
 (check-type bveq : (→ BV BV BV))
 (check-type (bveq (bv 1) (bv 1)) : BV -> (bv 1))