		Search-engine friendly clone of the ACL2 documentation.

Database

Flexprod-field-list->name-list

Lift flexprod-field->name to lists.

Signature
(flexprod-field-list->name-list fields) → names
Arguments: fields — Guard (flexprod-field-listp fields).
Returns: names — Type (symbol-listp names).

Definitions and Theorems

Function: flexprod-field-list->name-list

(defun flexprod-field-list->name-list (fields)
  (declare (xargs :guard (flexprod-field-listp fields)))
  (let ((__function__ 'flexprod-field-list->name-list))
    (declare (ignorable __function__))
    (b* (((when (endp fields)) nil)
         (name (flexprod-field->name (car fields)))
         ((unless (symbolp name))
          (raise "Internal error: malformed field name ~x0."
                 name))
         (names (flexprod-field-list->name-list (cdr fields))))
      (cons name names))))

Theorem: symbol-listp-of-flexprod-field-list->name-list

(defthm symbol-listp-of-flexprod-field-list->name-list
  (b* ((names (flexprod-field-list->name-list fields)))
    (symbol-listp names))
  :rule-classes :rewrite)