Comm-list
Fixtype of lists of Imp commands.
An empty command list captures a no-op,
called `skip' in typical formulations of Imp.
Subtopics
- Comm-list-equiv
- Basic equivalence relation for comm-list structures.
- Comm-listp
- (comm-listp x) recognizes lists where every element satisfies commp.
- Comm-list-fix
- (comm-list-fix x) is a usual ACL2::fty list fixing function.
