(vl-maybe-exprdist-strip x) → new-x
Function:
(defun vl-maybe-exprdist-strip (x) (declare (xargs :guard (vl-maybe-exprdist-p x))) (let ((__function__ 'vl-maybe-exprdist-strip)) (declare (ignorable __function__)) (vl-maybe-exprdist-case x :none (b* nil (change-vl-maybe-exprdist-none x)) :some (b* ((fty::val (vl-exprdist-strip x.val))) (change-vl-maybe-exprdist-some x :val fty::val)))))
Theorem:
(defthm vl-maybe-exprdist-p-of-vl-maybe-exprdist-strip (b* ((new-x (vl-maybe-exprdist-strip x))) (vl-maybe-exprdist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-maybe-exprdist-strip-of-vl-maybe-exprdist-fix-x (equal (vl-maybe-exprdist-strip (vl-maybe-exprdist-fix x)) (vl-maybe-exprdist-strip x)))
Theorem:
(defthm vl-maybe-exprdist-strip-vl-maybe-exprdist-equiv-congruence-on-x (implies (vl-maybe-exprdist-equiv x x-equiv) (equal (vl-maybe-exprdist-strip x) (vl-maybe-exprdist-strip x-equiv))) :rule-classes :congruence)