		Search-engine friendly clone of the ACL2 documentation.

Pseudo-event-formp

Pseudo-event-form-fix

Fixer for pseudo-event-formp.

Signature
(pseudo-event-form-fix x) → fixed-x
Arguments: x — Guard (pseudo-event-formp x).
Returns: fixed-x — Type (pseudo-event-formp fixed-x).

Definitions and Theorems

Function: pseudo-event-form-fix

(defun pseudo-event-form-fix (x)
  (declare (xargs :guard (pseudo-event-formp x)))
  (mbe :logic (if (pseudo-event-formp x) x '(_))
       :exec x))

Theorem: pseudo-event-formp-of-pseudo-event-form-fix

(defthm pseudo-event-formp-of-pseudo-event-form-fix
  (b* ((fixed-x (pseudo-event-form-fix x)))
    (pseudo-event-formp fixed-x))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-fix-when-pseudo-event-formp

(defthm pseudo-event-form-fix-when-pseudo-event-formp
  (implies (pseudo-event-formp x)
           (equal (pseudo-event-form-fix x) x)))