Raw constructor for honsed vl-tokstream-backup-p structures.
Syntax:
(honsed-vl-tokstream-backup tokens pstate)
This is identical to vl-tokstream-backup, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-vl-tokstream-backup (tokens pstate) (declare (xargs :guard (and (vl-tokenlist-p tokens) (vl-parsestate-p pstate)))) (mbe :logic (vl-tokstream-backup tokens pstate) :exec (hons tokens pstate)))