• 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.