• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
      • Break-rewrite
        • Monitor
        • Brr
        • Brr-commands
        • Dmr
        • With-brr-data
        • Geneqv
        • Refinement-failure
        • Break-lemma
        • Why-brr
        • Brr@
        • Cw-gstack
        • Ok-if
        • Windows-installation
        • Brr-near-missp
        • Monitored-runes
          • Unmonitor
          • Monitor!
        • Proof-builder
        • 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
    • Break-rewrite

    Monitored-runes

    Print the monitored runes and their break conditions

    Example and General Form:
    (monitored-runes)
    :monitored-runes

    This macro prints a list, each element of which is of the form (rune condition), showing each monitored rune and its current break condition.

    The list is printed to the comment window and not returned as the value (monitored-runes). The actual list is maintained in a wormhole managed by break-rewrite.

    Technically, the list of monitored runes is a locally bound variable of break-rewrite. The initial value of the variable is determined by its value in the containing scope of a call of break-rewrite. The value may be changed during interactions within the break, but it reverts to its old value upon return from break-rewrite. Thus if you monitor some runes, start a proof, adjust the monitored runes from within break-rewrite breaks in the proof attempt, and eventually return to the top-level, the value shown by :monitored-runes will be the same as it was when you started the proof.