|
|
|---|
|
|
|
|---|
Convert list of bits to a byte (big-endian).
;; Convert BITS (a list of 8 bits) into a byte in a big-endian fashion where ;; the first element of BITS becomes the most significant bit of the result, ;; and so on. (defund bits-to-byte (bits) (declare (xargs :guard (and (all-unsigned-byte-p 1 bits) (true-listp bits) (= 8 (len bits))))) (bvcat2 1 (nth 0 bits) 1 (nth 1 bits) 1 (nth 2 bits) 1 (nth 3 bits) 1 (nth 4 bits) 1 (nth 5 bits) 1 (nth 6 bits) 1 (nth 7 bits)))