The real toolchain, in your tab.
This playground runs disp's actual elaborator and its Rust evaluator (compiled to WebAssembly) — the same code that checks the test suite. Nothing is sent to a server.
Results live in the buffer, notebook-style: every definition shows its reduced value, every test its verdict, and edits re-check live once the kernel is warm. Values are explorable — click a number, string, or name to unfold the tree it stands for, click … to render deeper, − to fold a subterm back, and the tree button to pop the value into the reduction visualizer (folded names ride along as symbolic fruit).
The kernel arrives precompiled — a small snapshot of the checked module cache — so typed runs start in seconds. Don't trust it? : about a minute of the type system genuinely re-checking itself, right here.
⌘⏎ run file · ⇧⏎ run to cursor · ⌥W close tab (⌃W too, where the browser allows)