Extdecl-list
Fixtype of lists of external declarations.
External declarations are defined in extdecl.
This fixtype corresponds to external-declaration-list
in the grammar in [C].
Subtopics
- Extdecl-list-fix
- (extdecl-list-fix x) is a usual ACL2::fty list fixing function.
- Extdecl-listp
- (extdecl-listp x) recognizes lists where every element satisfies extdeclp.
- Extdecl-list-equiv
- Basic equivalence relation for extdecl-list structures.