		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-buf

(4vs-buf a) constructs a 4v-sexpr equivalent to (buf a).

Definitions and Theorems

Function: 4vs-buf

(defun 4vs-buf (a)
  (declare (xargs :guard t))
  (b* (((when (atom a))
        (if a (hons-list 'buf a) nil))
       (fn (car a)))
    (case fn
      ((f t x
          buf not and or xor iff ite ite* pullup)
       a)
      (t (hons-list 'buf a)))))

Theorem: 4v-sexpr-eval-of-4vs-buf

(defthm 4v-sexpr-eval-of-4vs-buf
  (equal (4v-sexpr-eval (4vs-buf a) env)
         (4v-unfloat (4v-sexpr-eval a env))))

Theorem: 4v-sexpr-vars-of-4vs-buf

(defthm 4v-sexpr-vars-of-4vs-buf
  (equal (4v-sexpr-vars (4vs-buf a))
         (4v-sexpr-vars a)))