		Search-engine friendly clone of the ACL2 documentation.

Faig-const->4v

Faig-const-alist->4v-alist

Signature
(faig-const-alist->4v-alist x) → *

Definitions and Theorems

Function: faig-const-alist->4v-alist

(defun faig-const-alist->4v-alist (x)
  (declare (xargs :guard t))
  (let ((__function__ 'faig-const-alist->4v-alist))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((atom (car x))
           (faig-const-alist->4v-alist (cdr x)))
          (t (cons (cons (caar x)
                         (faig-const->4v (cdar x)))
                   (faig-const-alist->4v-alist (cdr x)))))))

Theorem: lookup-faig-const-alist->4v-alist

(defthm lookup-faig-const-alist->4v-alist
 (equal (hons-assoc-equal k (faig-const-alist->4v-alist x))
        (and (hons-assoc-equal k x)
             (cons k
                   (faig-const->4v (cdr (hons-assoc-equal k x)))))))