		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Constraint-list-vars

Set of variables in a list of constraints.

Signature
(constraint-list-vars constrs) → vars
Arguments: constrs — Guard (constraint-listp constrs).
Returns: vars — Type (string-setp vars).

Definitions and Theorems

Function: constraint-list-vars

(defun constraint-list-vars (constrs)
  (declare (xargs :guard (constraint-listp constrs)))
  (let ((__function__ 'constraint-list-vars))
    (declare (ignorable __function__))
    (cond ((endp constrs) nil)
          (t (union (constraint-vars (car constrs))
                    (constraint-list-vars (cdr constrs)))))))

Theorem: string-setp-of-constraint-list-vars

(defthm string-setp-of-constraint-list-vars
  (b* ((vars (constraint-list-vars constrs)))
    (string-setp vars))
  :rule-classes :rewrite)