		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Pack-u64

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

Definitions and Theorems

Function: pack-u64

(defun pack-u64 (val)
  (declare (xargs :guard (n64p val)))
  (let ((__function__ 'pack-u64))
    (declare (ignorable __function__))
    (pack-u val 8)))

Theorem: byte-listp-of-pack-u64

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

Theorem: len-of-pack-u64-is-8

(defthm len-of-pack-u64-is-8
  (equal (len (pack-u64 x)) 8))