		Search-engine friendly clone of the ACL2 documentation.

Utilities

Bits-0-7

Inner loop for bits-0-31.

Signature
(bits-0-7 offset x acc) → *

Definitions and Theorems

Function: bits-0-7

(defun bits-0-7 (offset x acc)
  (declare (type unsigned-byte offset)
           (type (unsigned-byte 32) x))
  (let ((__function__ 'bits-0-7))
    (declare (ignorable __function__))
    (b* ((acc (if (logbitp 7 x)
                  (cons (+ 7 offset) acc)
                acc))
         (acc (if (logbitp 6 x)
                  (cons (+ 6 offset) acc)
                acc))
         (acc (if (logbitp 5 x)
                  (cons (+ 5 offset) acc)
                acc))
         (acc (if (logbitp 4 x)
                  (cons (+ 4 offset) acc)
                acc))
         (acc (if (logbitp 3 x)
                  (cons (+ 3 offset) acc)
                acc))
         (acc (if (logbitp 2 x)
                  (cons (+ 2 offset) acc)
                acc))
         (acc (if (logbitp 1 x)
                  (cons (+ 1 offset) acc)
                acc))
         (acc (if (logbitp 0 x)
                  (cons offset acc)
                acc)))
      acc)))

Theorem: bits-0-7-redef

(defthm bits-0-7-redef
  (implies (force (natp offset))
           (equal (bits-0-7 offset x acc)
                  (append (add-to-each offset (bits-between 0 8 x))
                          acc))))