suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix docs for define-judgment

Browse Source 
clarify the places where unquotes are not allowed
This commit is contained in:
Stephen Chang 2012-10-14 12:34:38 -04:00
parent be21153818
commit 4be0219855
1 changed files with 16 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
collects/redex/scribblings/ref.scrbl
View File

@ -43,6 +43,11 @@
[(_ args ...)
#'((tech (racketvarfont "term")) args ...)]
[x (identifier? #'x) #'(tech (racketvarfont "term"))]))
@(define-syntax (tttterm-no-unquote stx)
(syntax-case stx ()
[(_ args ...)
#'((tech (racketvarfont "term-without-unquote") #:key "term") args ...)]
[x (identifier? #'x) #'(tech (racketvarfont "term-without-unquote") #:key "term")]))
@(define-syntax (tterm stx)
(syntax-case stx ()
@ -1157,10 +1162,10 @@ and @racket[#f] otherwise.
rule-name]]
[conclusion (form-id pat/term ...)]
[premise (code:line (judgment-form-id pat/term ...) maybe-ellipsis)
(where @#,ttpattern @#,tttterm)
(where/hidden @#,ttpattern @#,tttterm)
(side-condition @#,tttterm)
(side-condition/hidden @#,tttterm)]
(where @#,ttpattern @#,tttterm-no-unquote)
(where/hidden @#,ttpattern @#,tttterm-no-unquote)
(side-condition @#,tttterm-no-unquote)
(side-condition/hidden @#,tttterm-no-unquote)]
[rule-name (code:line)
string
non-ellipsis-non-hypens-var]
@ -1231,7 +1236,8 @@ to compute all pairs with a given sum.
(judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2))]
A rule's @racket[where] and @racket[where/hidden] premises behave as in
@racket[reduction-relation] and @racket[define-metafunction].
@racket[reduction-relation] and @racket[define-metafunction] except the term
cannot use unquotes.
@examples[
#:eval redex-eval
(define-judgment-form nats
@ -1259,9 +1265,11 @@ A rule's @racket[where] and @racket[where/hidden] premises behave as in
A rule's @racket[side-condition] and @racket[side-condition/hidden] premises are similar
to those in @racket[reduction-relation] and @racket[define-metafunction], except that
they do not implicitly unquote their right-hand sides. In other words, a premise
of the form @racket[(side-condition exp)] is equivalent to the premise
@racket[(where #t exp)], except it does not typeset with the ``#t = '', as that would.
they do not implicitly unquote their right-hand sides. In other words, a premise
of the form @racket[(side-condition term)] is equivalent to the premise
@racket[(where #t term)], except it does not typeset with the ``#t = '', as that would.
Also, the term on the right-hand side cannot use unquotes so it is often convenient to
define a metafunction for these side-conditions.
A literal ellipsis may follow a judgment premise when a template in one of the
judgment's input positions contains a pattern variable bound at ellipsis-depth