		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Ppstate->bytes

Signature
(ppstate->bytes ppstate) → bytes
Returns: bytes — Type (byte-listp bytes).

Definitions and Theorems

Function: ppstate->bytes

(defun ppstate->bytes (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->bytes ppstate)
         nil)
       :exec (raw-ppstate->bytes ppstate)))

Theorem: byte-listp-of-ppstate->bytes

(defthm byte-listp-of-ppstate->bytes
  (b* ((bytes (ppstate->bytes ppstate)))
    (byte-listp bytes))
  :rule-classes :rewrite)

Theorem: true-listp-of-ppstate->bytes

(defthm true-listp-of-ppstate->bytes
  (b* ((bytes (ppstate->bytes ppstate)))
    (true-listp bytes))
  :rule-classes :type-prescription)

Theorem: ppstate->bytes-of-ppstate-fix-ppstate

(defthm ppstate->bytes-of-ppstate-fix-ppstate
  (equal (ppstate->bytes (ppstate-fix ppstate))
         (ppstate->bytes ppstate)))

Theorem: ppstate->bytes-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->bytes-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->bytes ppstate)
                  (ppstate->bytes ppstate-equiv)))
  :rule-classes :congruence)