		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Initializer-list-from-flds-vals

Signature
(initializer-list-from-flds-vals field-ids new-args) → l
Arguments: field-ids — Guard (identifier-listp field-ids).; new-args — Guard (expression-listp new-args).
Returns: l — Type (initializer-listp l).

Definitions and Theorems

Function: initializer-list-from-flds-vals

(defun initializer-list-from-flds-vals (field-ids new-args)
  (declare (xargs :guard (and (identifier-listp field-ids)
                              (expression-listp new-args))))
  (let ((__function__ 'initializer-list-from-flds-vals))
    (declare (ignorable __function__))
    (if (or (endp field-ids) (endp new-args))
        nil
      (cons (make-initializer :field (car field-ids)
                              :value (car new-args))
            (initializer-list-from-flds-vals (cdr field-ids)
                                             (cdr new-args))))))

Theorem: initializer-listp-of-initializer-list-from-flds-vals

(defthm initializer-listp-of-initializer-list-from-flds-vals
  (b* ((l (initializer-list-from-flds-vals field-ids new-args)))
    (initializer-listp l))
  :rule-classes :rewrite)