		Search-engine friendly clone of the ACL2 documentation.

Long-bits

Size of signed and unsigned long values, in bits.

Function: long-bits

(defun long-bits nil
  (declare (xargs :guard t))
  (let ((__function__ 'long-bits))
    (declare (ignorable __function__))
    64))

Theorem: posp-of-long-bits

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

Theorem: long-bits-multiple-of-char-bits

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

Theorem: long-bits-bound

(defthm long-bits-bound
  (b* ((?long-bits (long-bits)))
    (>= long-bits 32))
  :rule-classes :linear)