		Search-engine friendly clone of the ACL2 documentation.

Database

Flexprod-list->kind-list

Lift flexprod->kind to lists.

Signature
(flexprod-list->kind-list prods) → kinds
Arguments: prods — Guard (flexprod-listp prods).
Returns: kinds — Type (true-listp kinds).

Definitions and Theorems

Function: flexprod-list->kind-list

(defun flexprod-list->kind-list (prods)
  (declare (xargs :guard (flexprod-listp prods)))
  (let ((__function__ 'flexprod-list->kind-list))
    (declare (ignorable __function__))
    (cond ((endp prods) nil)
          (t (cons (flexprod->kind (car prods))
                   (flexprod-list->kind-list (cdr prods)))))))

Theorem: true-listp-of-flexprod-list->kind-list

(defthm true-listp-of-flexprod-list->kind-list
  (b* ((kinds (flexprod-list->kind-list prods)))
    (true-listp kinds))
  :rule-classes :rewrite)