		Search-engine friendly clone of the ACL2 documentation.

Llong-bits

Size of signed and unsigned llong values, in bits.

Function: llong-bits

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

Theorem: posp-of-llong-bits

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

Theorem: llong-bits-multiple-of-char-bits

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

Theorem: llong-bits-bound

(defthm llong-bits-bound
  (b* ((?llong-bits (llong-bits)))
    (>= llong-bits 64))
  :rule-classes :linear)