From 4d9cce823b9187755bafc0815623b29d2df705e7 Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Fri, 17 May 2013 15:26:38 -0500 Subject: [PATCH] fix docs for redex-generator --- collects/redex/scribblings/ref.scrbl | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/collects/redex/scribblings/ref.scrbl b/collects/redex/scribblings/ref.scrbl index f1831f03a0..da0ed90e2e 100644 --- a/collects/redex/scribblings/ref.scrbl +++ b/collects/redex/scribblings/ref.scrbl @@ -1950,11 +1950,18 @@ term that does not match @racket[pattern].} @examples[#:eval redex-eval - (define gen-sum (redex-generator nats (sum n_1 n_2 n_3) 5)) - (gen-sum) - (gen-sum) - (gen-sum) - (gen-sum)] + (define-language L + (nat ::= Z (S nat))) + (define-judgment-form L + #:mode (sum I I O) + [--------------- + (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]{