We actually generate a list of block items.
These can be regarded as forming a compound statement,
but lists of block items are compositional (via concatenation).
Described in atc-implementation.
It contains the variables in scope just after these block items,
i.e. the ones in scope for subsequent block items (if any).
This is nil if there are no subsequent block items,
which happens exactly when
these block items return a non-void type.
limit — pseudo-term
Symbolic limit value
that suffices for exec-block-item-list
to execute the block items completely.
The name of the theorem about exec-block-item-list
applied to the block items.
This theorem is one of the events in events.
It is nil if no theorem was generated,
because modular proof generation is not yet available
for some constructs;
eventually this will be never nil,
when modular proof generation covers
all the ATC-generated code.
