fix docs for redex-generator
This commit is contained in:
parent
4aed0897a2
commit
4d9cce823b
|
@ -1950,11 +1950,18 @@ term that does not match @racket[pattern].}
|
||||||
|
|
||||||
@examples[#:eval
|
@examples[#:eval
|
||||||
redex-eval
|
redex-eval
|
||||||
(define gen-sum (redex-generator nats (sum n_1 n_2 n_3) 5))
|
(define-language L
|
||||||
(gen-sum)
|
(nat ::= Z (S nat)))
|
||||||
(gen-sum)
|
(define-judgment-form L
|
||||||
(gen-sum)
|
#:mode (sum I I O)
|
||||||
(gen-sum)]
|
[---------------
|
||||||
|
(sum Z nat nat)]
|
||||||
|
[(sum nat_1 nat_2 nat_3)
|
||||||
|
-------------------------------
|
||||||
|
(sum (S nat_1) nat_2 (S nat_3))])
|
||||||
|
(define gen-sum (redex-generator L (sum nat_1 nat_2 nat_3) 3))
|
||||||
|
(for/list ([_ (in-range 5)])
|
||||||
|
(gen-sum))]
|
||||||
}
|
}
|
||||||
|
|
||||||
@defstruct[counterexample ([term any/c]) #:inspector #f]{
|
@defstruct[counterexample ([term any/c]) #:inspector #f]{
|
||||||
|
|
Loading…
Reference in New Issue
Block a user