		Search-engine friendly clone of the ACL2 documentation.
Primitive-values
Disjoint-primitive-values

The tagging keywords make all the primitive values disjoint.
Definitions and Theorems

Theorem: disjoint-primitive-values
(defthm disjoint-primitive-values
  (and (implies (boolean-valuep x)
                (and (not (char-valuep x))
                     (not (byte-valuep x))
                     (not (short-valuep x))
                     (not (int-valuep x))
                     (not (long-valuep x))
                     (not (float-valuep x))
                     (not (double-valuep x))
                     (not (floatx-valuep x))
                     (not (doublex-valuep x))))
       (implies (char-valuep x)
                (and (not (byte-valuep x))
                     (not (short-valuep x))
                     (not (int-valuep x))
                     (not (long-valuep x))
                     (not (float-valuep x))
                     (not (double-valuep x))
                     (not (floatx-valuep x))
                     (not (doublex-valuep x))))
       (implies (byte-valuep x)
                (and (not (short-valuep x))
                     (not (int-valuep x))
                     (not (long-valuep x))
                     (not (float-valuep x))
                     (not (double-valuep x))
                     (not (floatx-valuep x))
                     (not (doublex-valuep x))))
       (implies (short-valuep x)
                (and (not (int-valuep x))
                     (not (long-valuep x))
                     (not (float-valuep x))
                     (not (double-valuep x))
                     (not (floatx-valuep x))
                     (not (doublex-valuep x))))
       (implies (int-valuep x)
                (and (not (long-valuep x))
                     (not (float-valuep x))
                     (not (double-valuep x))
                     (not (floatx-valuep x))
                     (not (doublex-valuep x))))
       (implies (long-valuep x)
                (and (not (float-valuep x))
                     (not (double-valuep x))
                     (not (floatx-valuep x))
                     (not (doublex-valuep x))))
       (implies (float-valuep x)
                (and (not (double-valuep x))
                     (not (floatx-valuep x))
                     (not (doublex-valuep x))))
       (implies (double-valuep x)
                (and (not (floatx-valuep x))
                     (not (doublex-valuep x))))
       (implies (floatx-valuep x)
                (not (doublex-valuep x)))))