		Search-engine friendly clone of the ACL2 documentation.

Short-bits

Size of signed and unsigned short values, in bits.

Function: short-bits

(defun short-bits nil
  (declare (xargs :guard t))
  16)

Theorem: posp-of-short-bits

(defthm posp-of-short-bits
  (b* ((short-bits (short-bits)))
    (posp short-bits))
  :rule-classes :type-prescription)

Theorem: short-bits-multiple-of-char-bits

(defthm short-bits-multiple-of-char-bits
  (integerp (/ (short-bits) (char-bits)))
  :rule-classes :type-prescription)

Theorem: short-bits-bound

(defthm short-bits-bound
  (b* ((?short-bits (short-bits)))
    (>= short-bits 16))
  :rule-classes :linear)