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