		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-iff

(4vs-iff a b) constructs a sexpr representing (iff a b).

To make this better agree with sexpr-rewrite, I just implement this as the not of the xor.

Definitions and Theorems

Function: 4vs-iff

(defun 4vs-iff (a b)
  (declare (xargs :guard t))
  (4vs-not (4vs-xor a b)))

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

(defthm 4v-sexpr-eval-of-4vs-iff
  (equal (4v-sexpr-eval (4vs-iff a b) env)
         (4v-iff (4v-sexpr-eval a env)
                 (4v-sexpr-eval b env))))