		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Update-ppstate->chars-read

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

Definitions and Theorems

Function: update-ppstate->chars-read

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

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

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

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

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

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

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

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

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

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

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