(vl-tokenlist-fix x) → *
Function:
(defun vl-tokenlist-fix$inline (x) (declare (xargs :guard (vl-tokenlist-p x))) (let ((__function__ 'vl-tokenlist-fix)) (declare (ignorable __function__)) (mbe :logic (if (atom x) x (cons (if (vl-token-p (car x)) (car x) *vl-default-token*) (vl-tokenlist-fix (cdr x)))) :exec x)))
Theorem:
(defthm vl-tokenlist-p-of-vl-tokenlist-fix (vl-tokenlist-p (vl-tokenlist-fix x)))
Theorem:
(defthm vl-tokenlist-fix-when-vl-tokenlist-p (implies (vl-tokenlist-p x) (equal (vl-tokenlist-fix x) x)))
Theorem:
(defthm len-of-vl-tokenlist-fix (equal (len (vl-tokenlist-fix x)) (len x)))
Theorem:
(defthm consp-of-vl-tokenlist-fix (equal (consp (vl-tokenlist-fix x)) (consp x)))
Theorem:
(defthm cdr-of-vl-tokenlist-fix (equal (cdr (vl-tokenlist-fix (cons a x))) (vl-tokenlist-fix x)))
Theorem:
(defthm len-of-cdr-of-vl-tokenlist-fix (equal (len (cdr (vl-tokenlist-fix x))) (len (cdr x))))