9.2
1 The core calculus
All figures in this part are generated from the live Redex model every time the documentation is built, so they cannot drift from the code.
1.1 Grammar
The grammar of the Verse Calculus (Fig 1 of the paper, plus the Fig 4 contexts), as defined by the model’s VC language in "grammar.rkt", typeset toward the paper’s notation:
1.2 Reduction rules
The reduction rules (Fig 3), as defined by vc--> in "rules.rkt", typeset toward the paper’s notation:
The same rules in the model’s raw s-expression syntax — the notation that appears on the small gray line of every figure in the trace chapters:
