		Search-engine friendly clone of the ACL2 documentation.

Parser

Parstate->chars-read

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

Definitions and Theorems

Function: parstate->chars-read

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

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

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

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

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

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

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