• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
        • Instructions
        • Proof-builder-commands
        • Proof-builder-commands-short-list
        • Dive-into-macros-table
        • Verify
        • Define-pc-macro
        • Macro-command
        • Define-pc-help
        • Toggle-pc-macro
          • Define-pc-meta
          • Retrieve
          • Unsave
          • Proof-checker
        • Hons-and-memoization
        • Events
        • History
        • Parallelism
        • Programming
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Proof-builder

    Toggle-pc-macro

    Change an ordinary macro command to an atomic macro, or vice-versa

    Example:
    (toggle-pc-macro pro)

    Change pro from an atomic macro command to an ordinary one (or vice-versa, if pro happens to be an ordinary macro command)

    General Form:
    (toggle-pc-macro name &optional new-tp)

    If name is an atomic macro command then this turns it into an ordinary one, and vice-versa. However, if new-tp is supplied and not nil, then it should be the new type (the symbol macro or atomic-macro, in any package), or else there is no change.