		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Ppstate->lexeme

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

Definitions and Theorems

Function: ppstate->lexeme

(defun ppstate->lexeme (i ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp i)))
  (declare (xargs :guard (< i (ppstate->lexemes-length ppstate))))
  (mbe :logic
       (if (and (ppstatep ppstate)
                (< (nfix i)
                   (ppstate->lexemes-length ppstate)))
           (raw-ppstate->lexeme (nfix i) ppstate)
         (make-plexeme+span :lexeme (irr-plexeme)
                            :span (irr-position)))
       :exec (raw-ppstate->lexeme i ppstate)))

Theorem: plexeme+span-p-of-ppstate->lexeme

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