• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
      • Break-rewrite
      • 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
        • Accumulated-persistence
        • Cgen
        • Forward-chaining-reports
        • Proof-tree
        • Print-gv
        • Dmr
        • With-brr-data
        • Splitter
        • Guard-debug
        • Set-debugger-enable
        • Redo-flat
        • Time-tracker
        • Set-check-invariant-risk
        • Removable-runes
        • Efficiency
        • Explain-near-miss
        • Tail-biting
        • Failed-forcing
        • Sneaky
        • Invariant-risk
        • Failure
        • Measure-debug
        • Dead-events
        • Compare-objects
        • Prettygoals
        • Remove-hyps
        • Type-prescription-debugging
        • Pstack
        • Trace
        • Set-register-invariant-risk
        • Walkabout
        • Disassemble$
        • Nil-goal
        • Cw-gstack
        • Set-guard-msg
        • Find-lemmas
        • Watch
        • Quick-and-dirty-subsumption-replacement-step
        • Profile-all
        • Profile-ACL2
        • Set-print-gv-defaults
        • Minimal-runes
        • Spacewalk
        • Try-gl-concls
        • Near-misses
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Proof-builder

    Define-pc-help

    Define a macro command whose purpose is to print something

    Example:
    (define-pc-help pp ()
      (if (goals t)
          (io? proof-builder nil state
               (state-stack)
               (fms0 "~|~y0~|"
                     (list (cons #0
                                 (fetch-term (conc t)
                                             (current-addr t))))))
        (print-all-goals-proved-message state)))
    
    General Form:
    (define-pc-help name args &rest body)

    This defines a macro command named name, as explained further below. The body should (after removing optional declarations) be a form that returns state as its single value. Typically, it will just print something.

    What (define-pc-help name args &rest body) really does is to create a call of define-pc-macro that defines name to take arguments args, to have the declarations indicated by all but the last form in body, and to have a body that (via pprogn) first executes the form in the last element of body and then returns a call to the command skip (which will return (mv nil t state)).