(vl-typedef-strip x) → new-x
Function:
(defun vl-typedef-strip (x) (declare (xargs :guard (vl-typedef-p x))) (let ((__function__ 'vl-typedef-strip)) (declare (ignorable __function__)) (b* (((vl-typedef x) (vl-typedef-fix x))) (b* ((type (vl-datatype-strip x.type)) (atts ((lambda (x) (declare (ignore x)) nil) x.atts))) (change-vl-typedef x :type type :atts atts)))))
Theorem:
(defthm vl-typedef-p-of-vl-typedef-strip (b* ((new-x (vl-typedef-strip x))) (vl-typedef-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-typedef-strip-of-vl-typedef-fix-x (equal (vl-typedef-strip (vl-typedef-fix x)) (vl-typedef-strip x)))
Theorem:
(defthm vl-typedef-strip-vl-typedef-equiv-congruence-on-x (implies (vl-typedef-equiv x x-equiv) (equal (vl-typedef-strip x) (vl-typedef-strip x-equiv))) :rule-classes :congruence)