• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • 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-special-raw-definition-flag

    Ensure that named functions are flagged as having special raw definitions.

    Example Form:
    (ensure-special-raw-definition-flag my-fn your-fn)
    
    General Form:
    (ensure-special-raw-definition-flag fn1 fn2 ... fnk)

    where each fni is a literal symbol which should have a function definition. Each fni not already flagged as having a special raw definition is flagged as such. This idicates to interested parties that the "loop" definition of the function doesn't fully characterize the effects it has in raw lisp. 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.