• 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
    • 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
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Print-gv
• Guard
• Debugging

Set-print-gv-defaults

Set default keyword values for print-gv

Example Forms:
(set-print-gv-defaults :conjunct t)
(set-print-gv-defaults :conjunct t :substitute t)
(set-print-gv-defaults :conjunct t :substitute 20)
(set-print-gv-defaults :evisc-tuple
                       (evisc-tuple 4   ; print-level
                                    5   ; print-length
                                    (world-evisceration-alist state nil)
                                    nil ; hiding-cars
                                    ))
(set-print-gv-defaults :conjunct :restore
                       :substitute :restore
                       :evisc-tuple :restore)
(set-print-gv-defaults)

General Form:
(set-print-gv-defaults :conjunct c
                       :substitute s
                       :evisc-tuple e)

where any or all of c, s, and e may be the keyword, :restore, and otherwise these are as for print-gv. These forms set the defaults for the corresponding keyword arguments of the print-gv utility, where the value :restore restores the system defaults; see print-gv. Evaluation returns an error-triple whose value is an alist associating keywords with their current defaults. In particular, the call (set-print-gv-defaults) simply returns an error-triple with that alist as the value, without changing any defaults.

Thus, for example, if you submit the form

(set-print-gv-defaults :substitute t
                       :conjunct t
                       :evisc-tuple (evisc-tuple 3 4 nil nil))

then subsequently, if you submit the form :print-gv or (print-gv) it would be interpreted as follows.

(print-gv :substitute t
          :conjunct t
          :evisc-tuple (evisc-tuple 3 4 nil nil))

Of course, you can override your defaults, so that for example if you subsequently submit the form (print-gv :substitute nil) or the form (print-gv :substitute nil :evisc-tuple (print-gv-evisc-tuple)), these would be equivalent to submitting the following forms, respectively.

(print-gv :substitute nil
          :conjunct t
          :evisc-tuple (evisc-tuple 3 4 nil nil))
(print-gv :substitute nil
          :conjunct t
          :evisc-tuple (print-gv-evisc-tuple))