		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-to-faig

4v-sexpr-to-faig-alist

Convert a sexpr alist into an faig alist.

Definitions and Theorems

Function: 4v-sexpr-to-faig-alist-fn1

(defun 4v-sexpr-to-faig-alist-fn1 (x onoff optimizep)
  "Assumes ONOFF is fast."
  (declare (xargs :guard t))
  (cond ((atom x) nil)
        ((atom (car x))
         (4v-sexpr-to-faig-alist-fn1 (cdr x)
                                     onoff optimizep))
        (t (cons (cons (caar x)
                       (4v-sexpr-to-faig-fn1 (cdar x)
                                             onoff optimizep))
                 (4v-sexpr-to-faig-alist-fn1 (cdr x)
                                             onoff optimizep)))))

Function: 4v-sexpr-to-faig-alist-fn

(defun 4v-sexpr-to-faig-alist-fn (x onoff optimizep)
 "Assumes ONOFF is fast."
 (declare (xargs :guard t))
 (mbe
  :logic
  (cond ((atom x) nil)
        ((atom (car x))
         (4v-sexpr-to-faig-alist-fn (cdr x)
                                    onoff optimizep))
        (t (cons (cons (caar x)
                       (4v-sexpr-to-faig-fn (cdar x)
                                            onoff optimizep))
                 (4v-sexpr-to-faig-alist-fn (cdr x)
                                            onoff optimizep))))
  :exec
  (with-fast-alist onoff
                   (4v-sexpr-to-faig-alist-fn1 x onoff optimizep))))

Theorem: 4v-sexpr-to-faig-alist-fn1-removal

(defthm 4v-sexpr-to-faig-alist-fn1-removal
  (equal (4v-sexpr-to-faig-alist-fn1 x onoff optimizep)
         (4v-sexpr-to-faig-alist-fn x onoff optimizep)))