		Search-engine friendly clone of the ACL2 documentation.

Stv-restrict-alist

Stv-restrict-alist-aux

Signature
(stv-restrict-alist-aux name phase entries acc) → acc
Arguments: name — Guard (atom-listp name).; phase — Guard (natp phase).
Returns: acc — Type (alistp acc), given (alistp acc).

Definitions and Theorems

Function: stv-restrict-alist-aux

(defun stv-restrict-alist-aux (name phase entries acc)
 (declare (xargs :guard (and (atom-listp name) (natp phase))))
 (let ((__function__ 'stv-restrict-alist-aux))
   (declare (ignorable __function__))
   (b*
     (((when (atom entries)) acc)
      (name-at-phase
           (stv-suffix-signals name
                               (str::cat ".P" (str::natstr phase))))
      (val-at-phase (car entries))
      (acc (safe-pairlis-onto-acc name-at-phase val-at-phase acc)))
     (stv-restrict-alist-aux name (+ 1 phase)
                             (cdr entries)
                             acc))))

Theorem: alistp-of-stv-restrict-alist-aux

(defthm alistp-of-stv-restrict-alist-aux
  (implies
       (alistp acc)
       (b* ((acc (stv-restrict-alist-aux name phase entries acc)))
         (alistp acc)))
  :rule-classes :rewrite)