Update an alist from symbols to terms.
(atc-update-var-term-alist vars terms alist) → new-alist
Function:
(defun atc-update-var-term-alist (vars terms alist) (declare (xargs :guard (and (symbol-listp vars) (pseudo-term-listp terms) (symbol-pseudoterm-alistp alist)))) (let ((__function__ 'atc-update-var-term-alist)) (declare (ignorable __function__)) (append (pairlis$ (symbol-list-fix vars) (pseudo-term-list-fix terms)) (symbol-pseudoterm-alist-fix alist))))
Theorem:
(defthm symbol-pseudoterm-alistp-of-atc-update-var-term-alist (b* ((new-alist (atc-update-var-term-alist vars terms alist))) (symbol-pseudoterm-alistp new-alist)) :rule-classes :rewrite)