		Search-engine friendly clone of the ACL2 documentation.

Inline-mods

Vl-inline-rename-portdecl

Signature
(vl-inline-rename-portdecl x alist) → new-x
Arguments: x — Guard (vl-portdecl-p x).; alist — Guard (vl-renaming-alist-p alist).
Returns: new-x — Type (vl-portdecl-p new-x), given the guard.

Definitions and Theorems

Function: vl-inline-rename-portdecl

(defun vl-inline-rename-portdecl (x alist)
 (declare (xargs :guard (and (vl-portdecl-p x)
                             (vl-renaming-alist-p alist))))
 (let ((__function__ 'vl-inline-rename-portdecl))
  (declare (ignorable __function__))
  (b*
   ((new-name
     (or
      (cdr (hons-get (vl-portdecl->name x) alist))
      (raise
       "all portdecls should be bound, but no binding for ~x0.  Renaming Alist: ~x1"
       (vl-portdecl->name x)
       alist)
      (vl-portdecl->name x))))
   (change-vl-portdecl x :name new-name))))

Theorem: vl-portdecl-p-of-vl-inline-rename-portdecl

(defthm vl-portdecl-p-of-vl-inline-rename-portdecl
  (implies (and (vl-portdecl-p x)
                (vl-renaming-alist-p alist))
           (b* ((new-x (vl-inline-rename-portdecl x alist)))
             (vl-portdecl-p new-x)))
  :rule-classes :rewrite)