Major Section: MISCELLANEOUS
General Form: (get-wormhole-status name state)
Name should be the name of a wormhole (see wormhole). This function
returns an error triple (see error-triples) of the form
(mv nil s state), where s is the status of the named wormhole. The
status is obtained by reading the oracle in the ACL2 state.
This function makes the status of a wormhole visible outside the wormhole.
But since this function takes state and modifies it, the function may
only be used in contexts in which you may change state. Otherwise,
the wormhole status may stay in the wormhole. See wormhole-eval and
wormhole.
