A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

-->
::=
_
Abstract Machines
Abstracting Abstract Machines I
Abstracting Abstract Machines II
all-mods
alpha-equivalent?
Amb: A Redex Tutorial
any
apply-reduction-relation
apply-reduction-relation*
apply-reduction-relation/tag-with-names
arrow->pict
arrow-space
Automated Testing Benchmark
Behavior of binding forms
benchmark-logging-to
beta
bind
bind-exp
bind-name
bind?
Binding
binding forms
binding pattern
binding repetition
Binding repetitions
bmark-log-data
bmark-log-data-data
bmark-log-data?
bmark-log-directory
boolean
build-derivations
build-lw
caching-enabled?
calculus
CC Machine
check
check-metafunction
check-reduction-relation
check-redundancy
compatible-closure
compiled-lang?
computations
context-closure
Contexts, Values
counterexample
counterexample-term
counterexample?
coverage?
covered-cases
cross
curly-quotes-for-strings
current-cache-all?
current-render-pict-adjust
current-text
current-traced-metafunctions
Customization
dark-brush-color
dark-pen-color
dark-text-color
Debugging PLT Redex Programs
default-attempt-size
default-check-attempts
default-equiv
default-font-size
default-language
default-pretty-printer
default-style
default-white-square-bracket
define-extended-judgment-form
define-extended-language
define-judgment-form
define-language
define-metafunction
define-metafunction/extension
define-relation
define-rewrite
define-rewrite/compose
define-term
define-union-language
Defining a Language
Defining a Reduction Relation
delim-cont
delimit-ellipsis-arguments?
depth-dependent-order?
derivation
derivation-name
derivation-subs
derivation-term
derivation/ps
derivation?
Developing a Language
Developing a Language 2
Developing Metafunctions
Developing Type Judgments
environment
Exercises
Exercises
Exercises
Exercises
Exercises
Exercises
Exercises
exn:fail:redex:generation-failure?
exn:fail:redex:test
exn:fail:redex:test-source
exn:fail:redex:test-term
exn:fail:redex:test?
exn:fail:redex?
extend-language-show-extended-order
extend-language-show-union
extend-reduction-relation
Extended Exercises
Extending a Language: any
Finding the Benchmark Models
fresh
freshening
generate
generate-term
grammar-style
GUI
hide-hole
hole
hole
homemade-white-square-bracket
horizontal-bar-spacing
I
Imperative Extensions
in-domain?
in-hole
in-hole
include/rewrite
initial-char-width
initial-font-size
integer
IO-judgment-form?
judgment-form->pict
judgment-form-cases
judgment-form?
judgment-holds
just-after
just-before
Lab Abstracting Abstract Machines I
Lab Abstracting Abstract Machines II
Lab Contexts and Stores
Lab Designing Metafunctions
Lab Designing Reductions
Lab Machine Transitions
Lab Type Checking
label-font-size
label-space
label-style
language->pict
language-nts
Languages
lc-lang
let-poly
light-brush-color
light-pen-color
light-text-color
linebreaks
list-machine
literal-style
Logging
Long Tutorial
lw
lw->pict
lw-column
lw-column-span
lw-e
lw-line
lw-line-span
lw-metafunction?
lw-unq?
lw?
LWs
Macros and Typesetting
make-bind
make-counterexample
make-coverage
make-derivation
make-exn:fail:redex:test
make-lw
Managing Benchmark Modules
match-bindings
match?
metafunction->pict
metafunction-cases
metafunction-combine-contract-and-rules
metafunction-fill-acceptable-width
metafunction-font-size
metafunction-gap-space
metafunction-line-gap-space
metafunction-pict-style
metafunction-rule-gap-space
metafunction-style
metafunction-up/down-indent
metafunctions->pict
name
natural
non-terminal-gap-space
non-terminal-style
non-terminal-subscript-style
non-terminal-superscript-style
nothing
number
O
Objects: Problem
Objects: Solution
Other Relations
other-literal
paren-style
pattern
pattern-sequence
Patterns
Picts, PDF, & PostScript
Plotting
plug
poly-stlc
pretty-print-parameters
Problem: Binary Addition
Problem: Contracts
Problem: Finite State Machines
Problem: GC
Problem: Missionaries and Cannibals
Problem: Threads
Problem: Towers of Hanoi
Problem: Types
Program
Raising Exceptions
Random Testing
rbtrees
real
redex
redex
Redex Pattern, variable-prefix
Redex Pattern, variable-not-otherwise-mentioned
Redex Pattern, variable-except
Redex Pattern, variable
Redex Pattern, symbol
Redex Pattern, string
Redex Pattern, side-condition
Redex Pattern, real
Redex Pattern, pattern-sequence
Redex Pattern, other-literal
Redex Pattern, number
Redex Pattern, natural
Redex Pattern, name
Redex Pattern, integer
Redex Pattern, in-hole
Redex Pattern, hole
Redex Pattern, hide-hole
Redex Pattern, cross
Redex Pattern, boolean
Redex Pattern, any
Redex Pattern, _
redex-check
redex-generator
redex-let
redex-let*
redex-match
redex-match?
redex-pseudo-random-generator
redex/benchmark
redex/benchmark/models/all-info
redex/gui
redex/pict
redex/reduction-semantics
Redex: Practical Semantics Engineering
Reduction Relations
Reduction Relations
reduction-relation
reduction-relation->pict
reduction-relation->rule-names
reduction-relation-rule-extra-separation
reduction-relation-rule-line-separation
reduction-relation-rule-separation
reduction-relation?
reduction-rule-style/c
reduction-steps-cutoff
Reductions and Semantics
relation->pict
relation-clauses-combine
relation-coverage
Removing the Pink Background
render-judgment-form
render-language
render-language-nts
render-lw
render-metafunction
render-metafunctions
render-reduction-relation
render-reduction-relation-rules
render-relation
render-term
render-term/pretty-write
rule-pict-info->side-condition-pict
rule-pict-info-arrow
rule-pict-info-computed-label
rule-pict-info-label
rule-pict-info-lhs
rule-pict-info-rhs
rule-pict-info?
rule-pict-style
run-gen-and-check
run-gen-and-check/mods
run-results
run-results-cexps
run-results-time
run-results-tries
run-results?
Running Benchmark Models
rvm
scope
Semantics
semantics
set-arrow-pict!
set-cache-size!
set-lw-column!
set-lw-column-span!
set-lw-e!
set-lw-line!
set-lw-line-span!
set-lw-metafunction?!
set-lw-unq?!
shadow
show-derivations
side-condition
side-condition clause
side-condition/hidden clause
Solution: Binary Addition
Solution: Contracts
Solution: Finite State Machines
Solution: GC
Solution: Missionaries and Cannibals
Solution: Threads
Solution: Towers of Hanoi
Solution: Types
Standard reduction
stepper
stepper/seed
stlc
stlc-sub
string
struct:bind
struct:bmark-log-data
struct:counterexample
struct:derivation
struct:exn:fail:redex:test
struct:lw
struct:run-results
Subjection Reduction
substitute
Substitution
symbol
Syntax and Metafunctions
term
term
term->pict
term->pict/pretty-write
term-let
term-match
term-match/single
term-node-children
term-node-color
term-node-expr
term-node-height
term-node-labels
term-node-parents
term-node-set-color!
term-node-set-position!
term-node-set-red!
term-node-width
term-node-x
term-node-y
term-node?
Terms
test-->
test-->>
test-->>E
test-->>∃
test-equal
test-predicate
test-results
Testing
Testing Reduction Relations
Testing Typing
The Benchmark Models
The CC-CK Theorem
The CEK machine
The CEK-CK Theorem
The CK Machine
The Redex Reference
The structure of binding forms
The Theoretical Framework
to-lw
to-lw/stx
traces
traces/ps
Truth
Types
Types and Property Testing
Typesetting
Typesetting the Reduction Relation
Typing
union-reduction-relations
Value
variable
Variable Assignment
variable-except
variable-not-in
variable-not-otherwise-mentioned
variable-prefix
variables-not-in
What are Models
where clause
where-combine
where-make-prefix-pict
where/hidden clause
white-bracket-sizing
white-square-bracket
with
with-atomic-rewriter
with-compound-rewriter
with-compound-rewriters
with-unquote-rewriter