• 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
      • Output-controls
      • Macros
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
        • Oslib
        • Bridge
        • Clex
        • Tshell
        • Unsound-eval
        • Hacker
          • In-raw-mode
          • Progn+subsume-ttags
          • Ensure-program-only
            • Progn+touchable
            • Ensure-special-raw-definition-flag
            • Progn=touchable
            • Progn+redef
            • Ensure-program-only-flag
            • Defun-bridge
            • Assert-program-mode
            • Assert-no-special-raw-definition
            • With-redef-allowed
            • With-raw-mode
            • With-touchable
          • ACL2s-interface
          • Startup-banner
          • Command-line
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
        • Oslib
        • Bridge
        • Clex
        • Tshell
        • Unsound-eval
        • Hacker
          • In-raw-mode
          • Progn+subsume-ttags
          • Ensure-program-only
            • Progn+touchable
            • Ensure-special-raw-definition-flag
            • Progn=touchable
            • Progn+redef
            • Ensure-program-only-flag
            • Defun-bridge
            • Assert-program-mode
            • Assert-no-special-raw-definition
            • With-redef-allowed
            • With-raw-mode
            • With-touchable
          • ACL2s-interface
          • Startup-banner
          • Command-line
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Hacker

      Ensure-program-only

      Ensure that named functions are and remain in :PROGRAM mode.

      Example Form:
      (ensure-program-only my-fn your-fn)
      
      General Form:
      (ensure-program-only fn1 fn2 ... fnk)

      where each fni is a literal symbol which should have a program mode definition. An error is raised if any fni is not a program mode function. Also, each fni not already flagged as "program only" is flagged as such. This prevents it from being migrated to logic mode or being used in a macro. This is actually a combination of assert-program-mode and ensure-program-only-flag. This is a pseudo-event, meaning it can be used in an event context but does not (ever) change the world. Note that the normal undoing mechanism (see ubt) does not undo the effects of this pseudo-event.