		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Ppstate->char

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

Definitions and Theorems

Function: ppstate->char

(defun ppstate->char (i ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (natp i)))
  (declare (xargs :guard (< i (ppstate->chars-length ppstate))))
  (mbe :logic
       (if (and (ppstatep ppstate)
                (< (nfix i)
                   (ppstate->chars-length ppstate)))
           (raw-ppstate->char (nfix i) ppstate)
         (make-char+position :char 0
                             :position (irr-position)))
       :exec (raw-ppstate->char i ppstate)))

Theorem: char+position-p-of-ppstate->char

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