Checked cubical terms
Loading cubical C/WASM…
Expression
Context
Expression
Type
β and δ highlight every applicable site in the displayed term. Click a highlight to reduce that occurrence. Escape or Un-highlight cancels selection. Each step is kernel-checked; Back undoes it. Reduced terms stay expanded.
Edit native syntax
Definitions refer to the checked source registry by name. Editing does not change that registry.
Native C constructor opcodes, payloads, and operands. %n are term handles local to this replay session; each shared node is listed once. Zero marks an unused operand or the end of a list.