		Search-engine friendly clone of the ACL2 documentation.

File-layout

Vl-remove-illegitimate-tnames

Signature
(vl-remove-illegitimate-tnames x state) → (mv legitimate state)
Arguments: x — Guard (vl-tnamelist-p x).
Returns: legitimate — Type (vl-tnamelist-p legitimate).; state — Type (state-p1 state), given (force (state-p1 state)).

Definitions and Theorems

Function: vl-remove-illegitimate-tnames

(defun vl-remove-illegitimate-tnames (x state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (vl-tnamelist-p x)))
  (let ((__function__ 'vl-remove-illegitimate-tnames))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv nil state))
         ((mv car-legitp state)
          (vl-looks-like-legitimate-tname-p (car x)
                                            state))
         ((mv cdr-prime state)
          (vl-remove-illegitimate-tnames (cdr x)
                                         state))
         ((when car-legitp)
          (mv (cons (vl-tname-fix (car x)) cdr-prime)
              state)))
      (mv cdr-prime state))))

Theorem: vl-tnamelist-p-of-vl-remove-illegitimate-tnames.legitimate

(defthm vl-tnamelist-p-of-vl-remove-illegitimate-tnames.legitimate
  (b* (((mv ?legitimate acl2::?state)
        (vl-remove-illegitimate-tnames x state)))
    (vl-tnamelist-p legitimate))
  :rule-classes :rewrite)

Theorem: state-p1-of-vl-remove-illegitimate-tnames.state

(defthm state-p1-of-vl-remove-illegitimate-tnames.state
  (implies (force (state-p1 state))
           (b* (((mv ?legitimate acl2::?state)
                 (vl-remove-illegitimate-tnames x state)))
             (state-p1 state)))
  :rule-classes :rewrite)