• 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

    Unmonitor

    To stop monitoring a rule name

    Examples:
    (unmonitor '(:rewrite assoc-of-app))
    :unmonitor (:rewrite assoc-of-app)
    :unmonitor :all
    
    General Forms:
    (unmonitor rune)
    (unmonitor :all)

    Here, rune is a rune that is currently among those with break points installed. This function removes the break. See monitor.

    Subtle point: Because you may want to unmonitor a ``rune'' that is no longer a rune in the current ACL2 world, we don't actually check this about rune. We simply check that rune is currently monitored and remove it. If rune corresponds to no entry on the list of monitored runes we cause an error since it may indicate a misspelling.