• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
      • Break-rewrite
        • Monitor
        • Brr
          • Brr-evisc-tuple
          • Set-brr-evisc-tuple
          • Brr-commands
          • Dmr
          • With-brr-data
          • Geneqv
          • Refinement-failure
          • Break-lemma
          • Why-brr
          • Brr@
          • Cw-gstack
          • Ok-if
          • 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
      • Community
      • Std
      • Proof-automation
      • ACL2
      • Macro-libraries
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Brr
    • Brr-evisc-tuple
    • Set-evisc-tuple

    Set-brr-evisc-tuple

    Set the brr-evisc-tuple

    General Form:
    (set-brr-evisc-tuple ev state)

    where ev is either the keyword :default or a legal evisc-tuple. This function sets the evisceration tuple used by brr-commands. The current value can be retrieved with brr-evisc-tuple. The initial value is :default which means the :term evisceration tuple is used. To see how the brr-evisc-tuple is used see brr-evisc-tuple.

    Think of brr-evisc-tuple as a true global variable, not a locally bound variable of break-rewrite. In particular, if you set the brr-evisc-tuple inside a break-rewrite interactive break and eventually exit that break — either to enter a deeper break or return to a shallower break or to the ACL2 top-level — the brr-evisc-tuple will retain its chronologically most recent setting.

    The general command for setting any of the system evisc-tuples is set-evisc-tuple.