		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Ppstate->version

Signature
(ppstate->version ppstate) → version
Returns: version — Type (c::versionp version).

Definitions and Theorems

Function: ppstate->version

(defun ppstate->version (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->version ppstate)
         (c::version-c23))
       :exec (raw-ppstate->version ppstate)))

Theorem: versionp-of-ppstate->version

(defthm versionp-of-ppstate->version
  (b* ((version (ppstate->version ppstate)))
    (c::versionp version))
  :rule-classes :rewrite)

Theorem: ppstate->version-of-ppstate-fix-ppstate

(defthm ppstate->version-of-ppstate-fix-ppstate
  (equal (ppstate->version (ppstate-fix ppstate))
         (ppstate->version ppstate)))

Theorem: ppstate->version-ppstate-equiv-congruence-on-ppstate

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