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.
• Arbitrary evaluation order: choose CBV or CBN, or 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).