		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Update-ppstate->lexeme

Signature
(update-ppstate->lexeme i lexeme+span ppstate) → ppstate
Arguments: i — Guard (natp i).; lexeme+span — Guard (plexeme+span-p lexeme+span).
Returns: ppstate — Type (ppstatep ppstate).

Definitions and Theorems

Function: update-ppstate->lexeme

(defun update-ppstate->lexeme (i lexeme+span ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (and (natp i)
                             (plexeme+span-p lexeme+span))))
 (declare (xargs :guard (< i (ppstate->lexemes-length ppstate))))
 (b* ((ppstate (ppstate-fix ppstate)))
  (mbe
      :logic
      (if (< (nfix i)
             (ppstate->lexemes-length ppstate))
          (raw-update-ppstate->lexeme (nfix i)
                                      (plexeme+span-fix lexeme+span)
                                      ppstate)
        ppstate)
      :exec (raw-update-ppstate->lexeme i lexeme+span ppstate))))

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

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