Backend-independent syntax for bounded, stateful controller programs.
gap is an execution breakpoint used during search, never a finished program.
inductive ControlProgram
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.