		Search-engine friendly clone of the ACL2 documentation.

4vcases

Macro for cases on the 4-valued logic constants.

This looks like a case statement, except that t, f, and z match with (4vt), (4vf), and (4vz), respectively.

The x case should be the default (last) case. Anything other than t, f, or z will result in the default case; we typically use & or otherwise.

For example:

(defun 4v-not (a)
  (4vcases a
    (t (4vf))
    (f (4vt))
    (& (4vx))))

Is like writing:

(defun 4v-not (a)
  (cond ((eq a (4vt)) (4vf))
        ((eq a (4vf)) (4vt))
        (t (4vx))))

Definitions and Theorems

Function: 4vcases-cases

(defun 4vcases-cases (cases)
  (if (endp cases)
      nil
    (cons (list (case (caar cases)
                  ((t) '(eq 4vcases-var (4vt)))
                  (f '(eq 4vcases-var (4vf)))
                  (z '(eq 4vcases-var (4vz)))
                  (otherwise t))
                (cons 'check-vars-not-free
                      (cons '(4vcases-var)
                            (cons (cadar cases) 'nil))))
          (4vcases-cases (cdr cases)))))