		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Operations on the abstract syntax of PFCSes.

Expression-var-list: Lift expression-var to lists.
Lookup-definition: Look up a definition in a list of definitions.
Expression-sub: Abbreviation to construct a subtraction.
Definition-free-vars: Free variables in a definition.
Expression-vars: Variables in an expression.
Expression-list-vars: Variables in a list of expressions.
Expression-const/var-listp: Check if all the expressions in a list are constants or variables.
Constraint-list-vars: Variables in a list of constraints.
Expression-var-listp: Check if all the expressions in a list are variables.
Expression-neg: Abbreviation to construct a negation.
Constraint-vars: Variables in a constraint.