diff --git a/turnstile/scribblings/guide.scrbl b/turnstile/scribblings/guide.scrbl index 5d10df3..b71c7fd 100644 --- a/turnstile/scribblings/guide.scrbl +++ b/turnstile/scribblings/guide.scrbl @@ -338,17 +338,8 @@ language implementation: (λ ([x : Int][y : Int]) (f x y))) +) - 1 2)) - -@#reader scribble/comment-reader -(racketblock - (+ 1 (λ ([x : Int]) x)) - ;; 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 2) + (eval:error (+ 1 (λ ([x : Int]) x)))) @section{Extending a Language} @@ -360,6 +351,7 @@ how we can reuse the above implementation to implement a subtyping language. @label-code["A language with subtyping that reuses STLC" @(racketblock0 #:escape esc +(esc(lang turnstile)) (extends STLC #:except #%datum +) (define-base-types Top Num Nat) diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl index 1f13564..ec5cf4c 100644 --- a/turnstile/scribblings/reference.scrbl +++ b/turnstile/scribblings/reference.scrbl @@ -114,7 +114,7 @@ Turnstile pre-declares @racket[(define-syntax-category type)], which in turn @itemlist[ @item{@defform[(define-base-type base-type-name-id)]{ Defines a base type. A @racket[(define-base-type τ)] additionally defines: - @itemlist[@item{@racket[τ], an @literal{identifier} macro representing type @racket[τ].} + @itemlist[@item{@racket[τ], an identifier macro representing type @racket[τ].} @item{@racket[τ?], a predicate recognizing type @racket[τ].} @item{@racket[~τ], a @tech:pat-expander recognizing type @racket[τ].}]}} @item{@defform[(define-base-types base-type-name-id ...)]{Defines multiple base types.}}