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