		Search-engine friendly clone of the ACL2 documentation.

Vl-parsestate

Vl-parsestate-restore

Build a new parse-state whose alists are fast.

Signature
(vl-parsestate-restore pstate) → new-pstate
Arguments: pstate — Guard (vl-parsestate-p pstate).
Returns: new-pstate — Type (vl-parsestate-p new-pstate).

Definitions and Theorems

Function: vl-parsestate-restore

(defun vl-parsestate-restore (pstate)
  (declare (xargs :guard (vl-parsestate-p pstate)))
  (let ((__function__ 'vl-parsestate-restore))
    (declare (ignorable __function__))
    (b* (((vl-parsestate pstate) pstate))
      (change-vl-parsestate
           pstate
           :usertypes (make-fast-alist pstate.usertypes)))))

Theorem: vl-parsestate-p-of-vl-parsestate-restore

(defthm vl-parsestate-p-of-vl-parsestate-restore
  (b* ((new-pstate (vl-parsestate-restore pstate)))
    (vl-parsestate-p new-pstate))
  :rule-classes :rewrite)