From c0ce0debbef796ed0e31cc49590f595de2e0836f Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Wed, 10 Feb 2010 18:33:53 +0000 Subject: [PATCH] Improved documentation of `check-metafunction' svn: r18039 --- collects/redex/redex.scrbl | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 822c17f550..0df36e577a 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -1270,11 +1270,28 @@ when @scheme[relation] is a relation on @scheme[L] with @scheme[n] rules.} @defform/subs[(check-metafunction metafunction property kw-args ...) ([kw-arg (code:line #:attempts attempts-expr) (code:line #:retries retries-expr)]) - #:contracts ([property (-> any/c any/c)] + #:contracts ([property (-> (listof any/c) any/c)] [attempts-expr natural-number/c] [retries-expr natural-number/c])]{ -Like @scheme[check-reduction-relation] but for metafunctions.} +Like @scheme[check-reduction-relation] but for metafunctions. +@scheme[check-metafunction] calls @scheme[property] with lists +containing arguments to the metafunction.} +@examples[ +#:eval redex-eval + (define-language empty-lang) + + (random-seed 0) + + (define-metafunction empty-lang + Σ : number ... -> number + [(Σ) 0] + [(Σ number) number] + [(Σ number_1 number_2 number_3 ...) + (Σ ,(+ (term number_1) (term number_2)) number_3 ...)]) + + (check-metafunction Σ (λ (args) (printf "~s\n" args)) #:attempts 2)] + @defproc[(exn:fail:redex:generation-failure? [v any/c]) boolean?]{ Recognizes the exceptions raised by @scheme[generate-term], @scheme[redex-check], etc. when those forms are unable to produce