		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Update-ppstate->chars-unread

Signature
(update-ppstate->chars-unread chars-unread ppstate) → ppstate
Arguments: chars-unread — Guard (natp chars-unread).
Returns: ppstate — Type (ppstatep ppstate).

Definitions and Theorems

Function: update-ppstate->chars-unread

(defun update-ppstate->chars-unread (chars-unread ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp chars-unread)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->chars-unread (nfix chars-unread)
                                      ppstate)))

Theorem: ppstatep-of-update-ppstate->chars-unread

(defthm ppstatep-of-update-ppstate->chars-unread
 (b* ((ppstate (update-ppstate->chars-unread chars-unread ppstate)))
   (ppstatep ppstate))
 :rule-classes :rewrite)

Theorem: update-ppstate->chars-unread-of-nfix-chars-unread

(defthm update-ppstate->chars-unread-of-nfix-chars-unread
  (equal (update-ppstate->chars-unread (nfix chars-unread)
                                       ppstate)
         (update-ppstate->chars-unread chars-unread ppstate)))

Theorem: update-ppstate->chars-unread-nat-equiv-congruence-on-chars-unread

(defthm
  update-ppstate->chars-unread-nat-equiv-congruence-on-chars-unread
 (implies
  (acl2::nat-equiv chars-unread chars-unread-equiv)
  (equal (update-ppstate->chars-unread chars-unread ppstate)
         (update-ppstate->chars-unread chars-unread-equiv ppstate)))
 :rule-classes :congruence)

Theorem: update-ppstate->chars-unread-of-ppstate-fix-ppstate

(defthm update-ppstate->chars-unread-of-ppstate-fix-ppstate
 (equal
   (update-ppstate->chars-unread chars-unread (ppstate-fix ppstate))
   (update-ppstate->chars-unread chars-unread ppstate)))

Theorem: update-ppstate->chars-unread-ppstate-equiv-congruence-on-ppstate

(defthm
   update-ppstate->chars-unread-ppstate-equiv-congruence-on-ppstate
 (implies
  (ppstate-equiv ppstate ppstate-equiv)
  (equal (update-ppstate->chars-unread chars-unread ppstate)
         (update-ppstate->chars-unread chars-unread ppstate-equiv)))
 :rule-classes :congruence)