Raw constructor for honsed vl-tokstream-backup-p structures.
Syntax:
(honsed-vl-tokstream-backup tokens position 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 position pstate) (declare (xargs :guard (and (vl-tokenlist-p tokens) (natp position) (vl-parsestate-p pstate)))) (mbe :logic (vl-tokstream-backup tokens position pstate) :exec (hons tokens (hons position pstate))))