		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Update-ppstate->char

Signature
(update-ppstate->char i char+pos ppstate) → ppstate
Arguments: i — Guard (natp i).; char+pos — Guard (char+position-p char+pos).
Returns: ppstate — Type (ppstatep ppstate).

Definitions and Theorems

Function: update-ppstate->char

(defun update-ppstate->char (i char+pos ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (natp i)
                              (char+position-p char+pos))))
  (declare (xargs :guard (< i (ppstate->chars-length ppstate))))
  (b* ((ppstate (ppstate-fix ppstate)))
    (mbe :logic
         (if (< (nfix i)
                (ppstate->chars-length ppstate))
             (raw-update-ppstate->char (nfix i)
                                       (char+position-fix char+pos)
                                       ppstate)
           ppstate)
         :exec (raw-update-ppstate->char i char+pos ppstate))))

Theorem: ppstatep-of-update-ppstate->char

(defthm ppstatep-of-update-ppstate->char
  (b* ((ppstate (update-ppstate->char i char+pos ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)