• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
          • World
          • Io
          • Wormhole
            • Wormhole-eval
            • Wormhole-implementation
            • Make-wormhole-status
            • Get-wormhole-status
            • Set-wormhole-entry-code
              • Set-wormhole-data
              • Wormhole-data
              • Wormhole-statusp
              • Wormhole-p
              • Wormhole-entry-code
            • Programming-with-state
            • W
            • Set-state-ok
            • Random$
          • Memoize
          • Mbe
          • Io
          • Apply$
          • Defpkg
          • Mutual-recursion
          • Loop$
          • Programming-with-state
          • Arrays
          • Characters
          • Time$
          • Loop$-primer
          • Fast-alists
          • Defmacro
          • Defconst
          • Evaluation
          • Guard
          • Equality-variants
          • Compilation
          • Hons
          • ACL2-built-ins
          • Developers-guide
          • System-attachments
          • Advanced-features
          • Set-check-invariant-risk
          • Numbers
          • Irrelevant-formals
          • Efficiency
          • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
          • Redefining-programs
          • Lists
          • Invariant-risk
          • Errors
          • Defabbrev
          • Conses
          • Alists
          • Set-register-invariant-risk
          • Strings
          • Program-wrapper
          • Get-internal-time
          • Basics
          • Packages
          • Defmacro-untouchable
          • Primitive
          • <<
          • Revert-world
          • Set-duplicate-keys-action
          • Unmemoize
          • Symbols
          • Def-list-constructor
          • Easy-simplify-term
          • Defiteration
          • Defopen
          • Sleep
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Wormhole

    Set-wormhole-entry-code

    Sets the wormhole entry code in a wormhole status object

    General Form:  (set-wormhole-entry-code whs code)

    See wormhole. Whs should be a well-formed wormhole status and code should be :ENTER or :SKIP. This function returns a new status with the specified entry code but the same data as whs. It avoids unnecessary consing if the entry code for whs is already set to code. This function does not affect state or a wormhole's hidden status. It just returns a (possibly) new status object suitable as the value of the lambda expressions in wormhole-eval and wormhole.