		Search-engine friendly clone of the ACL2 documentation.

Utilities

60bits-0-3

Like bits-0-7, but since 8 doesn't divide 60, we have this goofy function for the final bits.

Signature
(60bits-0-3 offset x acc) → *

Definitions and Theorems

Function: 60bits-0-3

(defun 60bits-0-3 (offset x acc)
  (declare (type unsigned-byte offset)
           (type (unsigned-byte 60) x))
  (let ((__function__ '60bits-0-3))
    (declare (ignorable __function__))
    (b* ((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: 60bits-0-3-redef

(defthm 60bits-0-3-redef
  (implies (force (natp offset))
           (equal (60bits-0-3 offset x acc)
                  (append (add-to-each offset (bits-between 0 4 x))
                          acc))))