• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
      • Io
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Oslib
      • Std/io
      • 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
        • Startup-banner
        • Command-line
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Hacker

    Ensure-program-only-flag

    Ensure that given function names remain in :PROGRAM mode.

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

    where each fni is a literal symbol which should have a program mode definition. 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 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.