Byte-to-bits-little
Convert a byte to a list of bits (little-endian).
;; Convert a byte into a list of 8 bits. The least significant bit comes first
;; so this is "little endian." We could define this as (reverse-list (unpackbv
;; 8 1 (first bytes))), but that seems too complicated.
(defund byte-to-bits-little (byte)
(declare (xargs :guard (unsigned-byte-p 8 byte)))
(list (getbit 0 byte)
(getbit 1 byte)
(getbit 2 byte)
(getbit 3 byte)
(getbit 4 byte)
(getbit 5 byte)
(getbit 6 byte)
(getbit 7 byte)))
