MAKE-WORMHOLE-STATUS.html -- ACL2 Version 6.2

MAKE-WORMHOLE-STATUS

creates a wormhole status object from given status, entry code, and data

Major Section:  MISCELLANEOUS

General Form:  (make-wormhole-status whs code data)

See wormhole. Whs should be a well-formed wormhole status, code should be :ENTER or :SKIP, and data is arbitrary. This function returns a new status with the specified entry code and data, reusing whs if it is appropriate.