diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index 817f982..45abbf3 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -583,13 +583,16 @@
 
 (define-syntax define-basic-checked-id-stx
   (syntax-parser #:datum-literals (:)
-    [(_ τ:id : kind)
+    [(_ τ:id : kind
+        (~optional (~and #:no-provide (~parse no-provide? #'#t))))
      #:with #%tag (format-id #'kind "#%~a" #'kind)
      #:with τ? (mk-? #'τ)
      #:with τ-internal (generate-temporary #'τ)
      #:with τ-expander (format-id #'τ "~~~a" #'τ)
-     #'(begin
-         (provide τ (for-syntax τ? τ-expander))
+     #`(begin
+         #,@(if (attribute no-provide?)
+               #'()
+               #'((provide τ (for-syntax τ? τ-expander))))
          (begin-for-syntax
            (define (τ? t) ;(and (identifier? t) (free-identifier=? t #'τ-internal)))
              (syntax-parse t
@@ -648,9 +651,9 @@
      #:with τ-expander (format-id #'τ "~~~a" #'τ)
      #:with τ-expander* (format-id #'τ-expander "~a*" #'τ-expander)
      #`(begin
-         #,(if (attribute no-provide?)
-               #'(provide)
-               #'(provide τ (for-syntax τ-expander τ-expander* τ?)))
+         #,@(if (attribute no-provide?)
+               #'()
+               #'((provide τ (for-syntax τ-expander τ-expander* τ?))))
          (begin-for-syntax
            (define-syntax τ-expander
              (pattern-expander
@@ -840,7 +843,7 @@
                  (andmap (λ (τ) ((current-name=?) (car τs-lst) τ)) (cdr τs-lst)))))
          (define-syntax define-base-name
            (syntax-parser
-             [(_ (~var x id)) #'(define-basic-checked-id-stx x : name)]))
+             [(_ (~var x id) . rst) #'(define-basic-checked-id-stx x : name . rst)]))
          (define-syntax define-base-names
            (syntax-parser
              [(_ (~var x id) (... ...)) #'(begin (define-base-name x) (... ...))]))
@@ -853,6 +856,9 @@
 
 (define-syntax define-primop
   (syntax-parser #:datum-literals (:)
+    [(define-primop op:id : τ #:no-provide)
+     #:with op/tc (generate-temporary #'op)
+     #'(define-primop op/tc op : τ)]
     [(define-primop op:id : τ)
      #:with op/tc (generate-temporary #'op)
      #`(begin-
diff --git a/turnstile/scribblings/guide.scrbl b/turnstile/scribblings/guide.scrbl
index 2f8158a..2c4c179 100644
--- a/turnstile/scribblings/guide.scrbl
+++ b/turnstile/scribblings/guide.scrbl
@@ -1,6 +1,7 @@
 #lang scribble/manual
 
-@(require (for-label racket/base
+@(require scribble/example racket/sandbox
+          (for-label racket/base
                      (except-in turnstile/turnstile ⊢))
           "doc-utils.rkt" "common.rkt")
 
@@ -242,7 +243,7 @@ syntax object because the input type is automatically attached to that output.
 We also define an annotation form @racket[ann], which invokes the @racket[⇐]
 clause of a type rule.
 
-@section{Defining Primop}
+@section{Defining Primops}
 
 The previous sections have defined type rules for @racket[#%app] and @racket[λ],
 as well as a function type, but we cannot write any well-typed programs yet
@@ -322,6 +323,31 @@ language implementation:
     [_ #:error (type-error #:src #'x
                            #:msg "Unsupported literal: ~v" #'x)]]))]
 
+@(define the-eval
+  (parameterize ([sandbox-output 'string]
+                 [sandbox-error-output 'string]
+                 [sandbox-eval-limits #f])
+    (make-base-eval #:lang "../examples/stlc+lit.rkt")))
+
+@(examples #:eval the-eval 
+            (+ 1 2)
+            (((λ ([f : (→ Int Int Int)]) 
+                (λ ([x : Int][y : Int]) 
+                  (f x y))) 
+              +) 
+             1 2))
+
+@#reader scribble/comment-reader
+(racketblock
+  ;; eval:3.0: #%app: type mismatch: expected Int, given (→ Int Int)
+  ;;   expression: (λ ((x : Int)) x)
+  ;;   at: (λ ((x : Int)) x)
+  ;;   in: (#%app + 1 (λ ((x : Int)) x))
+  (+ 1 (λ ([x : Int]) x))
+)
+
+
+
 @section{Extending a Language}
 
 Imagine our language from the previous section is named @tt{STLC}. Since it
@@ -408,4 +434,4 @@ function, which is needed by conditional forms like @racket[if]. The
 @racket[if] definition uses the @racket[current-join] parameter, to
 make it reusable by other languages. Observe that the output type in the 
 @racket[if] definition uses @racket[unquote]. In general, all @tech:stx-template
-positions in Turnstile are @racket[quasisyntax]es.
\ No newline at end of file
+positions in Turnstile are @racket[quasisyntax]es.