Roadmap

• Draw the AST for the input term and synchronize mouse hovering: show the corresponding tokens for any AST node. (Possibly with vis.js?)
• Draw binding arrows (i.e., Stay diagrams) for any stage in the β-reduction.
• Flexible evaluation order: choose CBV or CBN.
  • Visually indicate the "next redex" where reduction will occur. Possibly show the next redex for all evaluation orders (not just the currently active one).
  • For full beta-reduction (nondeterministic), click a specific redex to reduce it.
• Encodings: expand names on click or "on demand," and otherwise preserve them through the reduction steps.
  • Optionally collapse names for legibility (i.e., rewrite \f. \x. f x back to ONE). (Perhaps using resugaring?)