Make-wormhole-status
Creates a wormhole status object from given status, entry code, and data
General Form: (make-wormhole-status whs code data)
See wormhole. Whs is generally a well-formed wormhole status
(but see below), code should be :ENTER or :SKIP, and data
is arbitrary. This function returns a new status with the specified entry
code and data. The result does not logically depend on whs, but if the
wormhole status corresponding to the given code and data is equal to whs,
then whs is returned, which will save a cons.
Warning: if data is large then the equality test can be slow.
That problem is avoided by passing whs = nil. For an example of this use
of nil in the ACL2 source code, see source function
save-ev-fncall-guard-er.
