Rulelist
Fixtype of lists of rules.
In the abstract syntax,
we use true lists of rules.
This corresponds to rulelist in [RFC:4],
abstracting away comments and blank space.
Subtopics
- Rulelist-fix
- (rulelist-fix x) is a usual ACL2::fty list fixing function.
- Rulelistp
- (rulelistp x) recognizes lists where every element satisfies rulep.
- Rulelist-equiv
- Basic equivalence relation for rulelist structures.
