Redex: Practical Semantics Engineering
PLT Redex consists of a domain-specific language for specifying reduction semantics, plus a suite of tools for working with the semantics.
This is a reference manual for Redex. See http://redex.racket-lang.org/ for a gentler overview. (See also the examples subdirectory in the redex collection.)
To load Redex use:
which provides all of the names documented in this library.
The module redex/reduction-semantics provides only the non-GUI portions of what is described in this manual (everything except the last two sections), making it suitable for use with racket scripts.
9 Removing the pink background from PLT Redex rendered picts and ps files