Status: 0 running/finished, 1 invalid, 2 breakpoint, 3 instruction exhaustion.
One action budget and one instruction budget are shared across all loops.
Status: 0 running/finished, 1 invalid, 2 breakpoint, 3 instruction exhaustion.
One action budget and one instruction budget are shared across all loops.
inductive ControlRun a
Constructors
For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.