		Search-engine friendly clone of the ACL2 documentation.

Parser

Parstate->chars-unread

Signature
(parstate->chars-unread parstate) → chars-unread
Returns: chars-unread — Type (natp chars-unread).

Definitions and Theorems

Function: parstate->chars-unread

(defun parstate->chars-unread (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (let ((__function__ 'parstate->chars-unread))
    (declare (ignorable __function__))
    (mbe :logic
         (if (parstatep parstate)
             (raw-parstate->chars-unread parstate)
           0)
         :exec (raw-parstate->chars-unread parstate))))

Theorem: natp-of-parstate->chars-unread

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

Theorem: parstate->chars-unread-of-parstate-fix-parstate

(defthm parstate->chars-unread-of-parstate-fix-parstate
  (equal (parstate->chars-unread (parstate-fix parstate))
         (parstate->chars-unread parstate)))

Theorem: parstate->chars-unread-parstate-equiv-congruence-on-parstate

(defthm parstate->chars-unread-parstate-equiv-congruence-on-parstate
  (implies (parstate-equiv parstate parstate-equiv)
           (equal (parstate->chars-unread parstate)
                  (parstate->chars-unread parstate-equiv)))
  :rule-classes :congruence)