Alternation
Fixtype of alternations.
In the abstract syntax,
for the alternatives described in [RFC:3.2]
and by rule alternation in [RFC:4],
we use true lists of concatenations.
We abstract away comments and blank space.
We also abstract away the restriction that
there be at least one alternation.
This restriction is captured by the notion of well-formed alternations.
Subtopics
- Alternationp
- (alternationp x) recognizes lists where every element satisfies concatenationp.
- Alternation-equiv
- Basic equivalence relation for alternation structures.
- Alternation-fix
- (alternation-fix x) is a usual ACL2::fty list fixing function.
