		Search-engine friendly clone of the ACL2 documentation.

Vl-scopeinfo-p

Vl-scopeinfo-make-fast

Ensure that the fast alists in a vl-scopeinfo are indeed fast alists.

Signature
(vl-scopeinfo-make-fast x) → *
Arguments: x — Guard (vl-scopeinfo-p x).

Definitions and Theorems

Function: vl-scopeinfo-make-fast

(defun vl-scopeinfo-make-fast (x)
 (declare (xargs :guard (vl-scopeinfo-p x)))
 (let ((__function__ 'vl-scopeinfo-make-fast))
  (declare (ignorable __function__))
  (mbe
    :logic x :exec
    (b* (((vl-scopeinfo x)))
      (change-vl-scopeinfo x
                           :locals (make-fast-alist x.locals)
                           :imports (make-fast-alist x.imports))))))