Step through an .mmb proof as the verifier's stack machine runs it, one
command at a time. The state shown is always before the highlighted step.
Everything runs in this tab: the file is parsed, verified and stepped locally, and never uploaded. It is kept in this browser's storage so that reloading the page returns you to the step you were on; o forgets it and opens another.
The left list is every declaration — sorts, terms, defs, axioms, theorems. Click a row, or filter by name, to open its proof. Inside a proof, click any term or theorem name — in the listing or inside an expression — to jump to it.
The command listing is on the left, the current step highlighted. On the right, Stack, Heap and Hypotheses show the machine's state: a red bar marks what the step is about to consume, a ▸ what the previous step pushed. The callout (bottom right) says what the active step does, in the applied declaration's own variables.
Expressions print in the source's notation (a -> b), recovered from the
mmb — no .mm1 needed. Each stack or heap slot is one of:
.mmbnpm start file.mmb; one the browser was handed has
to be handed over again, since it cannot be re-read without youA Thm or Unfold step runs a sub-machine that matches the theorem's conclusion against the target. Press u (or the callout's unify ⌄) to step through it; its own stack and heap appear beside the main ones.
Everything the verifier rejected, and where. Each part of a trail that names somewhere goes there — the declaration, the step within it, and the unify command within that. A failure in the declaration stream has no declaration to blame, so it is listed on its own.
Nothing wrong, and no reason to distrust the file — but the index is advisory, so parts of it can be absent while the proofs still verify. Where that leaves a name or an operator missing, it is noted here.
.mmbEverything runs in this tab — the file is parsed, verified and stepped locally, and never uploaded. It is kept in this browser's storage so a refresh does not need it again; the file button in the corner forgets it.
From a checkout, npm start path/to/file.mmb serves that file and
opens it here, and r re-reads it after a recompile.
| # | declaration | steps |
|---|