		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Pack-u32

Signature
(pack-u32 val) → bytes
Arguments: val — Guard (n32p val).
Returns: bytes — Type (byte-listp bytes).

Definitions and Theorems

Function: pack-u32

(defun pack-u32 (val)
  (declare (xargs :guard (n32p val)))
  (let ((__function__ 'pack-u32))
    (declare (ignorable __function__))
    (pack-u val 4)))

Theorem: byte-listp-of-pack-u32

(defthm byte-listp-of-pack-u32
  (b* ((bytes (pack-u32 val)))
    (byte-listp bytes))
  :rule-classes :rewrite)

Theorem: len-of-pack-u32-is-4

(defthm len-of-pack-u32-is-4
  (equal (len (pack-u32 x)) 4))