		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Ppstate->position

Signature
(ppstate->position ppstate) → position
Returns: position — Type (positionp position).

Definitions and Theorems

Function: ppstate->position

(defun ppstate->position (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->position ppstate)
         (irr-position))
       :exec (raw-ppstate->position ppstate)))

Theorem: positionp-of-ppstate->position

(defthm positionp-of-ppstate->position
  (b* ((position (ppstate->position ppstate)))
    (positionp position))
  :rule-classes :rewrite)