		Search-engine friendly clone of the ACL2 documentation.

Integer-predicates-alternative-definitions

Alternative definitions of predicates for integer values.

These provide alternative definitions of predicates like sintp in terms of valuep and value-kind.

Theorem: scharp-alt-def

(defthm scharp-alt-def
  (equal (scharp x)
         (and (valuep x)
              (equal (value-kind x) :schar))))

Theorem: ucharp-alt-def

(defthm ucharp-alt-def
  (equal (ucharp x)
         (and (valuep x)
              (equal (value-kind x) :uchar))))

Theorem: sshortp-alt-def

(defthm sshortp-alt-def
  (equal (sshortp x)
         (and (valuep x)
              (equal (value-kind x) :sshort))))

Theorem: ushortp-alt-def

(defthm ushortp-alt-def
  (equal (ushortp x)
         (and (valuep x)
              (equal (value-kind x) :ushort))))

Theorem: sintp-alt-def

(defthm sintp-alt-def
  (equal (sintp x)
         (and (valuep x)
              (equal (value-kind x) :sint))))

Theorem: uintp-alt-def

(defthm uintp-alt-def
  (equal (uintp x)
         (and (valuep x)
              (equal (value-kind x) :uint))))

Theorem: slongp-alt-def

(defthm slongp-alt-def
  (equal (slongp x)
         (and (valuep x)
              (equal (value-kind x) :slong))))

Theorem: ulongp-alt-def

(defthm ulongp-alt-def
  (equal (ulongp x)
         (and (valuep x)
              (equal (value-kind x) :ulong))))

Theorem: sllongp-alt-def

(defthm sllongp-alt-def
  (equal (sllongp x)
         (and (valuep x)
              (equal (value-kind x) :sllong))))

Theorem: ullongp-alt-def

(defthm ullongp-alt-def
  (equal (ullongp x)
         (and (valuep x)
              (equal (value-kind x) :ullong))))