Decl-list
Fixtype of lists of declarations.
Declarations are defined in decl.
This fixtype corresponds to declaration-list
in the grammar in [C],
which is under external definitions [C:6.9.1] [C:A.2.4].
Subtopics
- Decl-list-equiv
- Basic equivalence relation for decl-list structures.
- Decl-listp
- (decl-listp x) recognizes lists where every element satisfies declp.
- Decl-list-fix
- (decl-list-fix x) is a usual ACL2::fty list fixing function.
