		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Update-ppstate->position

Signature
(update-ppstate->position position ppstate) → ppstate
Arguments: position — Guard (positionp position).
Returns: ppstate — Type (ppstatep ppstate).

Definitions and Theorems

Function: update-ppstate->position

(defun update-ppstate->position (position ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (positionp position)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->position (position-fix position)
                                  ppstate)))

Theorem: ppstatep-of-update-ppstate->position

(defthm ppstatep-of-update-ppstate->position
  (b* ((ppstate (update-ppstate->position position ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->position-of-position-fix-position

(defthm update-ppstate->position-of-position-fix-position
  (equal (update-ppstate->position (position-fix position)
                                   ppstate)
         (update-ppstate->position position ppstate)))

Theorem: update-ppstate->position-position-equiv-congruence-on-position

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

Theorem: update-ppstate->position-of-ppstate-fix-ppstate

(defthm update-ppstate->position-of-ppstate-fix-ppstate
  (equal (update-ppstate->position position (ppstate-fix ppstate))
         (update-ppstate->position position ppstate)))

Theorem: update-ppstate->position-ppstate-equiv-congruence-on-ppstate

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