• 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

      Assert-program-mode

      Assert that given symbols name :PROGRAM mode functions.

      Example Form:
      (assert-program-mode my-fn your-fn)
      
      General Form:
      (assert-program-mode 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. This is a pseudo-event, meaning it can be used in an event context but does not (ever) change the world.