diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
new file mode 100644
index 0000000..5d567b5
--- /dev/null
+++ b/turnstile/examples/rosette/bv.rkt
@@ -0,0 +1,46 @@
+#lang turnstile
+;(require (only-in rosette bv bitvector))
+(require syntax/parse/define)
+(extends "../ext-stlc.rkt")
+(require (only-in "../stlc+reco+var.rkt" define-type-alias))
+
+(define-simple-macro (define-rosette-primop op:id : ty)
+  (begin
+    (require (only-in rosette [op op]))
+    (define-primop op : ty)))
+(define-simple-macro (define-rosette-primop* op1:id op2:id : ty)
+  (begin
+    (require (only-in rosette [op1 op2]))
+    (define-primop op2 : ty)))
+
+(provide BVPred)
+
+(define-base-type BV) ; represents actual bitvectors
+
+; a predicate recognizing bv's of a certain size
+(define-type-alias BVPred (→ BV Bool))
+
+(define-rosette-primop bv : (→ Int BVPred BV))
+(define-rosette-primop bv? : (→ BV Bool))
+(define-rosette-primop bitvector : (→ Int BVPred))
+(define-rosette-primop bitvector? : (→ BVPred Bool))
+(define-rosette-primop* bitvector bvpred : (→ Int BVPred))
+(define-rosette-primop* bitvector? bvpred? : (→ BVPred Bool))
+
+(define-rosette-primop bveq : (→ BV BV Bool))
+(define-rosette-primop bvslt : (→ BV BV Bool))
+(define-rosette-primop bvult : (→ BV BV Bool))
+(define-rosette-primop bvsle : (→ BV BV Bool))
+(define-rosette-primop bvule : (→ BV BV Bool))
+(define-rosette-primop bvsgt : (→ BV BV Bool))
+(define-rosette-primop bvugt : (→ BV BV Bool))
+(define-rosette-primop bvsge : (→ BV BV Bool))
+(define-rosette-primop bvuge : (→ BV BV Bool))
+
+(define-rosette-primop bvnot : (→ BV BV))
+;; (require (postfix-in - (rosette))
+;; (define-typed-syntax bvand
+;;   [(_ e ...+)
+;;    [⊢ [[e ≫ e-] ⇐ : BV] ...]
+;;    --------
+;;    [⊢ [[_ ≫ (bvand- e- ...)] ⇒ : Bool]]])
diff --git a/turnstile/examples/tests/rosette/bv-tests.rkt b/turnstile/examples/tests/rosette/bv-tests.rkt
new file mode 100644
index 0000000..41154fe
--- /dev/null
+++ b/turnstile/examples/tests/rosette/bv-tests.rkt
@@ -0,0 +1,28 @@
+#lang s-exp "../../rosette/bv.rkt"
+(require "../rackunit-typechecking.rkt")
+
+(check-type bv : (→ Int BVPred BV))
+(typecheck-fail (bv "1" 2) #:with-msg "expected Int, given String")
+(check-type (bv 1 (bvpred 2)) : BV -> (bv 1 (bvpred 2)))
+
+(check-type bitvector : (→ Int BVPred))
+(check-type (bitvector 3) : BVPred)
+(typecheck-fail ((bitvector 4) 1))
+(check-type ((bitvector 4) (bv 10 (bvpred 4))) :  Bool)
+
+;; same as above, but with bvpred
+(check-type bvpred : (→ Int BVPred))
+(check-type (bvpred 3) : BVPred)
+(typecheck-fail ((bvpred 4) 1))
+(check-type ((bvpred 4) (bv 10 (bvpred 4))) :  Bool)
+
+(typecheck-fail (bitvector? "2"))
+(check-type (bitvector? (bitvector 10)) : Bool -> #t)
+(typecheck-fail (bvpred? "2"))
+(check-type (bvpred? (bvpred 10)) : Bool -> #t)
+
+(check-type (bveq (bv 1 (bvpred 3)) (bv 1 (bvpred 3))) : Bool -> #t)
+(typecheck-fail (bveq (bv 1 (bvpred 3)) 1))
+(check-type (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3))) : Bool) ; -> exn
+
+