		Search-engine friendly clone of the ACL2 documentation.

Annotation-list

Fixtype of lists of Leo annotations.

This is an ordinary fty::deflist.

Annotation-list-fix: (annotation-list-fix x) is a usual ACL2::fty list fixing function.
Annotation-list-equiv: Basic equivalence relation for annotation-list structures.
Annotation-listp: (annotation-listp x) recognizes lists where every element satisfies annotationp.