• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
      • Break-rewrite
      • Proof-builder
      • Accumulated-persistence
      • Cgen
      • Forward-chaining-reports
      • Proof-tree
      • Print-gv
      • Dmr
      • With-brr-data
      • Splitter
        • Set-splitter-output
        • Splitter-output
        • 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
        • Theories
        • Rule-classes
        • Proof-builder
        • Recursion-and-induction
        • Hons-and-memoization
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
          • Break-rewrite
          • Proof-builder
          • Accumulated-persistence
          • Cgen
          • Forward-chaining-reports
          • Proof-tree
          • Print-gv
          • Dmr
          • With-brr-data
          • Splitter
            • Set-splitter-output
            • Splitter-output
            • 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
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Splitter

      Splitter-output

      Status for reporting of splitter rules

      See splitter for a discussion of splitter rules. See set-splitter-output for how to turn off, or on, the reporting of splitter rules. When splitter-output is off, because either prove output is inhibited (see set-inhibit-output-lst) or (set-splitter-output nil) has been invoked, then the value of (splitter-output) is nil. Otherwise, such reporting is on and the value is non-nil.