		Search-engine friendly clone of the ACL2 documentation.

Parse-utils

Vl-tokenlist-fix

Signature
(vl-tokenlist-fix x) → *
Arguments: x — Guard (vl-tokenlist-p x).

Definitions and Theorems

Function: vl-tokenlist-fix$inline

(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: vl-tokenlist-p-of-vl-tokenlist-fix

(defthm vl-tokenlist-p-of-vl-tokenlist-fix
  (vl-tokenlist-p (vl-tokenlist-fix x)))

Theorem: vl-tokenlist-fix-when-vl-tokenlist-p

(defthm vl-tokenlist-fix-when-vl-tokenlist-p
  (implies (vl-tokenlist-p x)
           (equal (vl-tokenlist-fix x) x)))

Theorem: len-of-vl-tokenlist-fix

(defthm len-of-vl-tokenlist-fix
  (equal (len (vl-tokenlist-fix x))
         (len x)))

Theorem: consp-of-vl-tokenlist-fix

(defthm consp-of-vl-tokenlist-fix
  (equal (consp (vl-tokenlist-fix x))
         (consp x)))

Theorem: cdr-of-vl-tokenlist-fix

(defthm cdr-of-vl-tokenlist-fix
  (equal (cdr (vl-tokenlist-fix (cons a x)))
         (vl-tokenlist-fix x)))

Theorem: len-of-cdr-of-vl-tokenlist-fix

(defthm len-of-cdr-of-vl-tokenlist-fix
  (equal (len (cdr (vl-tokenlist-fix x)))
         (len (cdr x))))