Search-engine friendly clone of the
ACL2 documentation
.
Top
Abstract-syntax
Expression-fixtypes
Expression-list
Fixtype of lists of Leo expressions.
This is an ordinary
fty::deflist
.
Subtopics
Expression-list-equiv
Basic equivalence relation for
expression-list
structures.
Expression-listp
(expression-listp x)
recognizes lists where every element satisfies
expressionp
.
Expression-list-fix
(expression-list-fix x)
is a usual
ACL2::fty
list fixing function.