		Search-engine friendly clone of the ACL2 documentation.

Maybe-lit-fix

(maybe-lit-fix x) is the identity for maybe-litps, or coerces any non-litp to nil.

Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.

Function: maybe-lit-fix$inline

(defun maybe-lit-fix$inline (x)
  (declare (xargs :guard (maybe-litp x)))
  (mbe :logic (if x (lit-fix x) nil)
       :exec x))

Theorem: maybe-litp-of-maybe-lit-fix

(defthm maybe-litp-of-maybe-lit-fix
  (maybe-litp (maybe-lit-fix x))
  :rule-classes (:rewrite :type-prescription))

Theorem: maybe-lit-fix-when-maybe-litp

(defthm maybe-lit-fix-when-maybe-litp
  (implies (maybe-litp x)
           (equal (maybe-lit-fix x) x)))

Theorem: maybe-lit-fix-under-iff

(defthm maybe-lit-fix-under-iff
  (iff (maybe-lit-fix x) x))

Theorem: maybe-lit-fix-under-lit-equiv

(defthm maybe-lit-fix-under-lit-equiv
  (lit-equiv (maybe-lit-fix x) x))