• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
        • Term
        • Ld
          • Wormhole
            • Wormhole-eval
            • Wormhole-status
            • Wormhole-programming-tips
            • Wormhole-implementation
            • Sync-ephemeral-whs-with-persistent-whs
            • Get-persistent-whs
            • Set-persistent-whs-and-ephemeral-whs
            • Make-wormhole-status
            • Set-wormhole-entry-code
            • Set-wormhole-data
              • Wormhole-data
              • Wormhole-entry-code
              • Wormhole-statusp
              • Wormhole-p
            • Ld-skip-proofsp
            • Ld-redefinition-action
            • Lp
            • Ld-error-action
            • Ld-history
            • Guarantees-of-the-top-level-loop
            • Ld-post-eval-print
            • Ld-keyword-aliases
            • Current-package
            • Ld-query-control-alist
            • Ld-prompt
            • Keyword-commands
            • Redef+
            • Rebuild
            • Prompt
            • Ld-pre-eval-print
            • Calling-ld-in-bad-contexts
            • P!
            • Ld-pre-eval-filter
            • Ld-error-triples
            • Ld-evisc-tuple
            • Ld-verbose
            • A!
            • Default-print-prompt
            • Reset-ld-specials
            • Ld-always-skip-top-level-locals
            • Ld-missing-input-ok
            • Redef
            • Redef!
            • Redef-
            • I-am-here
            • Abort!
          • Hints
          • Type-set
          • Ordinals
          • Clause
          • ACL2-customization
          • With-prover-step-limit
          • Set-prover-step-limit
          • With-prover-time-limit
          • Local-incompatibility
          • Set-case-split-limitations
          • Subversive-recursions
          • Specious-simplification
          • Defsum
          • Gcl
          • Oracle-timelimit
          • Thm
          • Defopener
          • Case-split-limitations
          • Set-gc-strategy
          • Default-defun-mode
          • Top-level
          • Reader
          • Ttags-seen
          • Adviser
          • Ttree
          • Abort-soft
          • Defsums
          • Gc$
          • With-timeout
          • Coi-debug::fail
          • Expander
          • Gc-strategy
          • Coi-debug::assert
          • Sin-cos
          • Def::doc
          • Syntax
          • Subversive-inductions
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Wormhole

    Set-wormhole-data

    Sets the wormhole data object in a wormhole status object

    General Form:  (set-wormhole-data whs data)

    See wormhole. Whs should be a well-formed wormhole status; data is arbitrary. This function returns a new status with the same entry code as whs but with the new data. This function does not affect state or a wormhole's persistent-whs or ephemeral-whs. It just returns a (possibly) new status object suitable as the value of the lambda expressions in wormhole-eval and wormhole.