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
"close.rkt""common.rkt""extend-lookup.rkt""tc-common.rkt"#:...bind#:exports#:refers-to-->::=_Abstract MachinesAbstracting Abstract Machinesall-modsalpha-equivalent?Amb: A Redex Tutorialanyapply-reduction-relationapply-reduction-relation*apply-reduction-relation/tag-with-namesarrow->pictarrow-spaceAutomated Testing Benchmarkbenchmark-logging-tobindbind-expbind-namebind?Binding Formsbinding formsBinding Repetitionsbmark-log-databmark-log-data-databmark-log-data?bmark-log-directorybooleanbuild-derivationsbuild-lwcaching-enabled?calculusCC Machinecheckcheck-metafunctioncheck-reduction-relationcheck-redundancycompatible-closurecompiled-lang?Compound Forms with Binderscomputationscontext-closureContexts, Valuescounterexamplecounterexample-termcounterexample?coverage?covered-casescrosscurly-quotes-for-stringscurrent-cache-all?current-render-pict-adjustcurrent-textcurrent-traced-metafunctionsCustomizationdark-brush-colordark-pen-colordark-text-colorDebugging PLT Redex Programsdefault-attempt-sizedefault-check-attemptsdefault-equivdefault-font-sizedefault-languagedefault-pretty-printerdefault-styledefault-white-square-bracketdefine-extended-judgment-formdefine-extended-languagedefine-judgment-formdefine-languagedefine-metafunctiondefine-metafunction/extensiondefine-relationdefine-rewritedefine-rewrite/composedefine-termdefine-union-languageDefining a LanguageDefining a Reduction Relationdelim-contdelimit-ellipsis-arguments?depth-dependent-order?derivationderivation-namederivation-subsderivation-termderivation/psderivation?Developing a LanguageDeveloping a Language 2Developing MetafunctionsDeveloping Type JudgmentsEllipses in Binding FormsenvironmentExercisesExercisesExercisesExercisesExercisesexn:fail:redex:generation-failure?exn:fail:redex:testexn:fail:redex:test-sourceexn:fail:redex:test-termexn:fail:redex:test?exn:fail:redex?extend-language-show-extended-orderextend-language-show-unionextend-reduction-relationExtended ExercisesExtending a Language: anyfill-betweenFinding the Benchmark Modelsfreshgenerategenerate-termgrammar-styleGUIhide-holeholeholehomemade-white-square-brackethorizontal-bar-spacingIImperative Extensionsin-domain?in-holein-holeinclude/rewriteinitial-char-widthinitial-font-sizeintegerIO-judgment-form?judgment-form->pictjudgment-form-casesjudgment-form-show-rule-namesjudgment-form?judgment-holdsjust-afterjust-beforeLab Contexts and StoresLab Designing MetafunctionsLab Designing ReductionsLab Machine TransitionsLab Type Checkinglabel-font-sizelabel-spacelabel-stylelanguage->pictlanguage-ntsLanguageslc-langlet-polylight-brush-colorlight-pen-colorlight-text-colorlinebreakslist-machineliteral-styleLoggingLong Tutoriallwlw->pictlw-columnlw-column-spanlw-elw-linelw-line-spanlw-metafunction?lw-unq?lw?LWsMacros and Typesettingmake-bindmake-binding-hashmake-counterexamplemake-coveragemake-derivationmake-exn:fail:redex:testmake-immutable-binding-hashmake-lwManaging Benchmark Modulesmatch-bindingsmatch?metafunctionmetafunction->pictmetafunction-arrow-pictmetafunction-casesmetafunction-combine-contract-and-rulesmetafunction-fill-acceptable-widthmetafunction-font-sizemetafunction-gap-spacemetafunction-line-gap-spacemetafunction-pict-stylemetafunction-rule-gap-spacemetafunction-stylemetafunction-up/down-indentmetafunctions->pictmf-applyMultiple Variables in a Single Scopenamenaturalnon-terminal-gap-spacenon-terminal-stylenon-terminal-subscript-stylenon-terminal-superscript-stylenothingnumberOOther Relationsother-literalparen-stylepatternpattern-sequencePatternsPicts, PDF, & PostScriptPlottingplugpoly-stlcpretty-print-parametersProblem: Binary AdditionProblem: ContractsProblem: Finite State MachinesProblem: GCProblem: Missionaries and CannibalsProblem: ObjectsProblem: ThreadsProblem: Towers of HanoiProblem: TypesProgramRaising ExceptionsRandom TestingrbtreesrealredexredexRedex Pattern, variable-prefixRedex Pattern, variable-not-otherwise-mentionedRedex Pattern, variable-exceptRedex Pattern, variableRedex Pattern, symbolRedex Pattern, stringRedex Pattern, side-conditionRedex Pattern, realRedex Pattern, pattern-sequenceRedex Pattern, other-literalRedex Pattern, numberRedex Pattern, naturalRedex Pattern, nameRedex Pattern, integerRedex Pattern, in-holeRedex Pattern, holeRedex Pattern, hide-holeRedex Pattern, crossRedex Pattern, booleanRedex Pattern, anyRedex Pattern, _redex-checkredex-enumredex-generatorredex-indexredex-letredex-let*redex-matchredex-match?redex-pseudo-random-generatorredex/benchmarkredex/benchmark/models/all-inforedex/guiredex/pictredex/reduction-semanticsRedex: Practical Semantics EngineeringReduction RelationsReduction Relationsreduction-relationreduction-relation->pictreduction-relation->rule-namesreduction-relation-rule-extra-separationreduction-relation-rule-line-separationreduction-relation-rule-separationreduction-relation?reduction-rule-style/creduction-steps-cutoffReductions and Semanticsrelation->pictrelation-clauses-combinerelation-coverageRemoving the Pink Backgroundrender-judgment-formrender-languagerender-language-ntsrender-lwrender-metafunctionrender-metafunctionsrender-reduction-relationrender-reduction-relation-rulesrender-relationrender-termrender-term/pretty-writerule-pict-info->side-condition-pictrule-pict-info-arrowrule-pict-info-computed-labelrule-pict-info-labelrule-pict-info-lhsrule-pict-info-rhsrule-pict-info?rule-pict-stylerun-gen-and-checkrun-gen-and-check/modsrun-resultsrun-results-cexpsrun-results-timerun-results-triesrun-results?Running Benchmark Modelsrvmsc-linebreaksscopeSemanticssemanticsset-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?!shadowshow-derivationsside-conditionside-condition clauseside-condition/hidden clauseSolution: Binary AdditionSolution: ContractsSolution: Finite State MachinesSolution: GCSolution: Missionaries and CannibalsSolution: ObjectsSolution: ThreadsSolution: Towers of HanoiSolution: TypesStandard reductionstepperstepper/seedstlcstlc-substringstruct:bindstruct:bmark-log-datastruct:counterexamplestruct:derivationstruct:exn:fail:redex:teststruct:lwstruct:run-resultsSubjection ReductionsubstituteSubstitutionsymbolSyntax and Metafunctionstermtermterm->pictterm->pict/pretty-writeterm-letterm-matchterm-match/singleterm-node-childrenterm-node-colorterm-node-exprterm-node-heightterm-node-labelsterm-node-parentsterm-node-set-color!term-node-set-position!term-node-set-red!term-node-widthterm-node-xterm-node-yterm-node?Termstest-->test-->>test-->>Etest-->>∃test-equaltest-judgment-holdstest-predicatetest-resultsTestingTesting Reduction RelationsTesting TypingThe Benchmark ModelsThe CC-CK TheoremThe CEK machineThe CEK-CK TheoremThe CK MachineThe Redex ReferenceThe Theoretical Frameworkto-lwto-lw/stxtracestraces/psTruthTypesTypes and Property TestingTypesettingTypesetting the Reduction RelationTypingunion-reduction-relationsValuevariableVariable Assignmentvariable-exceptvariable-not-invariable-not-otherwise-mentionedvariable-prefixvariables-not-inWhat are Modelswhere clausewhere-combinewhere-make-prefix-pictwhere/error clausewhere/hidden clausewhite-bracket-sizingwhite-square-bracketwithwith-atomic-rewriterwith-atomic-rewriterswith-compound-rewriterwith-compound-rewriterswith-unquote-rewriter