From e569710e63627ab105dc0c61fb524a002cb1db76 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Fri, 8 Aug 2014 17:41:06 -0500 Subject: [PATCH] fix rule reference in tutoral, also spell-check closes PR 14676 --- .../redex-doc/redex/scribblings/tut.scrbl | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/tut.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/tut.scrbl index e1d1f54398..ce4f44fed9 100644 --- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/tut.scrbl +++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/tut.scrbl @@ -304,7 +304,7 @@ the language @racket[L] with a new non-terminal The @racket[define-extended-language] form accepts the name of the new language, the name of the extended -langauge and then a series of non-terminals just +language and then a series of non-terminals just like @racket[define-language]. In the extended language, we can give all of the @@ -360,7 +360,7 @@ the shape @racket[(types Γ e t)]. (types Γ (amb e ...) num)])] The first clause gives -the typing rule for aplication expressions, saying +the typing rule for application expressions, saying that if @racket[e_1] has the type @racket[(→ t_2 t_3)] and @racket[e_2] has the type @racket[t_2], then the application expression @@ -370,8 +370,8 @@ Similarly, the other clauses give the typing rules for all of the other forms in the language. Most of the rules use use @racket[types], or give base types to atomic -expressions, but the fourth rule is worth a special look. It says that -if a variable typechecks in some environment, then it also type +expressions, but the fifth rule is worth a special look. It says that +if a variable type checks in some environment, then it also type checks in an extended environment, provided that the environment extension does not use the variable in question. @@ -447,7 +447,7 @@ has, returning a list of them (in this case, just one). In general, the @racket[judgment-holds] form's first argument is an instance of some judgment-form that should have concrete terms for the @racket[I] positions in the mode spec, and patterns -in the positions labelled @racket[O]. Then, the second position +in the positions labeled @racket[O]. Then, the second position in @racket[judgment-holds] is an expression that can use the pattern variables inside those @racket[O] positions. The result of @racket[judgment-holds] will be a list of terms, one for @@ -744,7 +744,7 @@ The first rule replaces @racket[if0] expressions when the test position is @racket[0] by the second subexpression (the true branch). It uses the @racket[in-hole] pattern, the Redex notation for context decomposition. In this case, it decomposes a program into some @racket[P] with -an approriate @racket[if0] expression inside, and then the right-hand +an appropriate @racket[if0] expression inside, and then the right-hand side of the rule places @racket[e_1] into the same context. The rule for the false branch should apply when the test position is @@ -941,7 +941,7 @@ a pattern (@racket[e] in this case), and a Racket expression that returns a boolean. It randomly generates expressions matching the pattern and then invokes the expression in an attempt to elicit @racket[#f] from the Racket expression. -We can also ask redex-check how good of a job it is doing. +We can also ask @racket[redex-check] how good of a job it is doing. Specifically, this expression re-runs the same random test, but this time sets up some instrumenting infrastructure to determine how many of the reduction rules fire during the @@ -961,7 +961,7 @@ fired. (redex-check Ev e (progress-holds? (term e)))) (covered-cases c))] -Not many of them! To improve coverage, we can tell redex-check +Not many of them! To improve coverage, we can tell @racket[redex-check] to try generating expressions using the patterns on the left-hand side of the rules to generate programs, and then check to see if progress for each of the expressions in the program: @@ -1034,7 +1034,7 @@ program have the same type. @section{Typesetting the Reduction Relation} -Redex's typsetting facilities accept languages, metafunctions, reduction relations, +Redex's typesetting facilities accept languages, metafunctions, reduction relations, and judgment-forms and produce typeset output that can be included directly into a figure in a paper. @@ -1063,9 +1063,9 @@ then we can use the pict primitives to combine typeset fragments into a larger w Generally speaking, Redex has reasonable default ways to typeset its definitions, except when they escapes to Racket. In that case, -it typsets the code in a fixed-width font and makes the background pink to call our +it typesets the code in a fixed-width font and makes the background pink to call our attention to it. While it is possible to use @racket[with-unquote-rewriter] to -tell Redex how to typset those regions, often it is easier to define a metafunction +tell Redex how to typeset those regions, often it is easier to define a metafunction and call it. In this case, we can use @racket[different] (defined earlier). @m[(define if0-false-rule