		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.
Constrel: Fixtype of relation constraints.
Constraint-constrels: Set of relation constraints in a constraint.
Constraint-list-constrels: Set of relation constraints in a list of constraints.
Constraint-rels: Set of (names of) relations in a constraint.
Constraint-list-rels: Set of (names of) relations in a list of constraints.
Expression-sub: Abbreviation to construct a subtraction.
Expression-const/var-listp: Check if all the expressions in a list are constants or variables.
Expression-var-listp: Check if all the expressions in a list are variables.
Expression-neg: Abbreviation to construct a negation.
Expression-list-vars: Set of variables in a list of expressions.
Expression-vars: Set of variables in an expression.
Definition-free-vars: Set of free variables in a definition.
Constraint-vars: Set of variables in a constraint.
Constraint-list-vars: Set of variables in a list of constraints.
Constrel-set: Fixtype of osets of relation constraints.