		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4v-to-characterp

Signature
(4v-to-characterp upper lower) → c
Arguments: upper — Guard (booleanp upper).; lower — Guard (booleanp lower).
Returns: c — Type (characterp c).

Definitions and Theorems

Function: 4v-to-characterp

(defun 4v-to-characterp (upper lower)
  (declare (xargs :guard (and (booleanp upper)
                              (booleanp lower))))
  (let ((__function__ '4v-to-characterp))
    (declare (ignorable __function__))
    (if (equal upper lower)
        (if upper #\1 #\0)
      (if (and upper (not lower)) #\x #\z))))

Theorem: characterp-of-4v-to-characterp

(defthm characterp-of-4v-to-characterp
  (b* ((c (4v-to-characterp upper lower)))
    (characterp c))
  :rule-classes :rewrite)