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

Uses examples' in explanation of judgment form where' clauses

Browse Source
This commit is contained in:
Casey Klein 2011-08-08 16:14:00 -05:00
parent d2a58bc05f
commit 29ffea3b76
1 changed files with 6 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
collects/redex/redex.scrbl
View File

@ -1069,7 +1069,7 @@ legtimate inputs according to @racket[metafunction-name]'s contract,
and @racket[#f] otherwise. and @racket[#f] otherwise.
} }
@defform/subs[#:literals (I O where etc.) @defform/subs[#:literals (I O where where/hidden etc.)
(define-judgment-form language (define-judgment-form language
option ... option ...
rule ...) rule ...)
@ -1088,7 +1088,8 @@ and @racket[#f] otherwise.
conclusion]] conclusion]]
[conclusion (form-id pat/term ...)] [conclusion (form-id pat/term ...)]
[premise (judgment-form-id pat/term ...) [premise (judgment-form-id pat/term ...)
(where @#,ttpattern @#,tttterm)] (where @#,ttpattern @#,tttterm)
(where/hidden @#,ttpattern @#,tttterm)]
[pat/term @#,ttpattern [pat/term @#,ttpattern
@#,tttterm] @#,tttterm]
[dashes --- [dashes ---
@ -1147,9 +1148,9 @@ to compute all pairs with a given sum.
(sumr n_1 n_2 n_3)]) (sumr n_1 n_2 n_3)])
(judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2))] (judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2))]
A rule's @racket[where] clause premises behave as in @racket[reduction-relation] A rule's @racket[where] and @racket[where/hidden] premises behave as in
and @racket[define-metafunction]. @racket[reduction-relation] and @racket[define-metafunction].
@interaction[ @examples[
#:eval redex-eval #:eval redex-eval
(define-judgment-form nats (define-judgment-form nats
#:mode (le I I) #:mode (le I I)