		Search-engine friendly clone of the ACL2 documentation.

Parser-states

Parstate->chars-read

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

Definitions and Theorems

Function: parstate->chars-read$inline

(defun parstate->chars-read$inline (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard t))
  (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$inline parstate)))
    (natp chars-read))
  :rule-classes (:rewrite :type-prescription))