|
|
|---|
|
|
|
|---|
Make a wormhole's status visible outside the wormhole
General Form: (get-wormhole-status name state)
Warning: This function is deprecated and will likely be eliminated after ACL2 Version 8.6.
This function has been renamed to be get-persistent-whs, i.e.,
“persistent wormhole status”. While the old name is still
defined, we recommend that you use the new name because it clarifies which
status object is being fetched: the persistent one (i.e., the one that must be
logically read from the ACL2 oracle and which survives the exit from a
wormhole to the next entrance to that wormhole) and not the ephemeral one
sometimes found in