[scribblings] respond to comments on PR #29

- add `#lang turnstile` to Sec 2.7
- use eval:error in @examples[]
- remove @literal
This commit is contained in:
Ben Greenman 2016-09-30 10:14:01 -04:00
parent 9116cfd5a2
commit ffa0a05e26
2 changed files with 4 additions and 12 deletions

View File

@ -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)

View File

@ -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.}}