		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-constraint

Abstract a *constraint to a list of constraints.

Signature
(abs-*-constraint trees) → constraints
Arguments: trees — Guard (abnf::tree-listp trees).
Returns: constraints — Type (constraint-list-resultp constraints).

Definitions and Theorems

Function: abs-*-constraint

(defun abs-*-constraint (trees)
  (declare (xargs :guard (abnf::tree-listp trees)))
  (let ((__function__ 'abs-*-constraint))
    (declare (ignorable __function__))
    (b* (((when (endp trees)) nil)
         ((okf constraint)
          (abs-constraint (car trees)))
         ((okf constraints)
          (abs-*-constraint (cdr trees))))
      (cons constraint constraints))))

Theorem: constraint-list-resultp-of-abs-*-constraint

(defthm constraint-list-resultp-of-abs-*-constraint
  (b* ((constraints (abs-*-constraint trees)))
    (constraint-list-resultp constraints))
  :rule-classes :rewrite)

Theorem: constraint-listp-of-abs-*-constraint

(defthm constraint-listp-of-abs-*-constraint
  (b* ((?constraints (abs-*-constraint trees)))
    (implies (not (reserrp constraints))
             (constraint-listp constraints))))

Theorem: abs-*-constraint-of-tree-list-fix-trees

(defthm abs-*-constraint-of-tree-list-fix-trees
  (equal (abs-*-constraint (abnf::tree-list-fix trees))
         (abs-*-constraint trees)))

Theorem: abs-*-constraint-tree-list-equiv-congruence-on-trees

(defthm abs-*-constraint-tree-list-equiv-congruence-on-trees
  (implies (abnf::tree-list-equiv trees trees-equiv)
           (equal (abs-*-constraint trees)
                  (abs-*-constraint trees-equiv)))
  :rule-classes :congruence)