		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Ppstate->lexemes-unread

Signature
(ppstate->lexemes-unread ppstate) → lexemes-unread
Returns: lexemes-unread — Type (natp lexemes-unread).

Definitions and Theorems

Function: ppstate->lexemes-unread

(defun ppstate->lexemes-unread (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->lexemes-unread ppstate)
         0)
       :exec (raw-ppstate->lexemes-unread ppstate)))

Theorem: natp-of-ppstate->lexemes-unread

(defthm natp-of-ppstate->lexemes-unread
  (b* ((lexemes-unread (ppstate->lexemes-unread ppstate)))
    (natp lexemes-unread))
  :rule-classes (:rewrite :type-prescription))

Theorem: ppstate->lexemes-unread-of-ppstate-fix-ppstate

(defthm ppstate->lexemes-unread-of-ppstate-fix-ppstate
  (equal (ppstate->lexemes-unread (ppstate-fix ppstate))
         (ppstate->lexemes-unread ppstate)))

Theorem: ppstate->lexemes-unread-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->lexemes-unread-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->lexemes-unread ppstate)
                  (ppstate->lexemes-unread ppstate-equiv)))
  :rule-classes :congruence)