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.
The first run that touches the type system elaborates and re-verifies the kernel: about a minute of genuine self-checking, cached for the session. , or pick the raw tree-calculus example for instant gratification.
⌘⏎ run file · ⇧⏎ run to cursor · the ▸ prompt below evaluates expressions
▸