		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Read-vars-values

Lift read-var-value to lists.

Signature
(read-vars-values vars cstate) → vals
Arguments: vars — Guard (identifier-listp vars).; cstate — Guard (cstatep cstate).
Returns: vals — Type (value-list-resultp vals).

Definitions and Theorems

Function: read-vars-values

(defun read-vars-values (vars cstate)
  (declare (xargs :guard (and (identifier-listp vars)
                              (cstatep cstate))))
  (let ((__function__ 'read-vars-values))
    (declare (ignorable __function__))
    (b* (((when (endp vars)) nil)
         ((okf val)
          (read-var-value (car vars) cstate))
         ((okf vals)
          (read-vars-values (cdr vars) cstate)))
      (cons val vals))))

Theorem: value-list-resultp-of-read-vars-values

(defthm value-list-resultp-of-read-vars-values
  (b* ((vals (read-vars-values vars cstate)))
    (value-list-resultp vals))
  :rule-classes :rewrite)

Theorem: len-of-read-vars-values

(defthm len-of-read-vars-values
  (b* ((?vals (read-vars-values vars cstate)))
    (implies (not (reserrp vals))
             (equal (len vals) (len vars)))))

Theorem: error-info-wfp-of-read-vars-values

(defthm error-info-wfp-of-read-vars-values
  (b* ((?vals (read-vars-values vars cstate)))
    (implies (reserrp vals)
             (error-info-wfp vals))))

Theorem: read-vars-values-of-identifier-list-fix-vars

(defthm read-vars-values-of-identifier-list-fix-vars
  (equal (read-vars-values (identifier-list-fix vars)
                           cstate)
         (read-vars-values vars cstate)))

Theorem: read-vars-values-identifier-list-equiv-congruence-on-vars

(defthm read-vars-values-identifier-list-equiv-congruence-on-vars
  (implies (identifier-list-equiv vars vars-equiv)
           (equal (read-vars-values vars cstate)
                  (read-vars-values vars-equiv cstate)))
  :rule-classes :congruence)

Theorem: read-vars-values-of-cstate-fix-cstate

(defthm read-vars-values-of-cstate-fix-cstate
  (equal (read-vars-values vars (cstate-fix cstate))
         (read-vars-values vars cstate)))

Theorem: read-vars-values-cstate-equiv-congruence-on-cstate

(defthm read-vars-values-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (read-vars-values vars cstate)
                  (read-vars-values vars cstate-equiv)))
  :rule-classes :congruence)