• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
        • Defun
          • Xargs
            • Guard
              • Verify-guards
              • Mbe
              • Set-guard-checking
              • Ec-call
              • Print-gv
                • Set-print-gv-defaults
                • The
                • Guards-and-evaluation
                • Guard-debug
                • Set-check-invariant-risk
                • Guard-evaluation-table
                • Guard-evaluation-examples-log
                • Guard-example
                • Defthmg
                • Invariant-risk
                • With-guard-checking
                • Guard-miscellany
                • Guard-holders
                • Guard-formula-utilities
                • Set-verify-guards-eagerness
                • Guard-quick-reference
                • Set-register-invariant-risk
                • Guards-for-specification
                • Guard-evaluation-examples-script
                • Guard-introduction
                • Program-only
                • Non-exec
                • Set-guard-msg
                • Safe-mode
                • Set-print-gv-defaults
                  • Guard-theorem-example
                  • With-guard-checking-event
                  • With-guard-checking-error-triple
                  • Guard-checking-inhibited
                  • Extra-info
                • Otf-flg
                • Normalize
                • Measure
              • Mutual-recursion
              • Defun-mode
              • Rulers
              • Defun-inline
              • Defun-nx
              • Defund
              • Set-ignore-ok
              • Set-well-founded-relation
              • Set-measure-function
              • Set-irrelevant-formals-ok
              • Defun-notinline
              • Set-bogus-defun-hints-ok
              • Defund-nx
              • Defun$
              • Defund-notinline
              • Defnd
              • Defn
              • Defund-inline
              • Set-bogus-measure-ok
            • Verify-guards
            • Table
            • Mutual-recursion
            • Memoize
            • Make-event
            • Include-book
            • Encapsulate
            • Defun-sk
            • Defttag
            • Defstobj
            • Defpkg
            • Defattach
            • Defabsstobj
            • Defchoose
            • Progn
            • Defconst
            • Verify-termination
            • Redundant-events
            • Defmacro
            • Skip-proofs
            • In-theory
            • Embedded-event-form
            • Value-triple
            • Comp
            • Local
            • Defthm
            • Progn!
            • Defevaluator
            • Theory-invariant
            • Assert-event
            • Defun-inline
            • Project-dir-alist
            • Partial-encapsulate
            • Define-trusted-clause-processor
            • Defproxy
            • Defexec
            • Defun-nx
            • Defthmg
            • Defpun
            • Defabbrev
            • Set-table-guard
            • Name
            • Defrec
            • Add-custom-keyword-hint
            • Regenerate-tau-database
            • Defcong
            • Deftheory
            • Defaxiom
            • Deftheory-static
            • Defund
            • Evisc-table
            • Verify-guards+
            • Logical-name
            • Profile
            • Defequiv
            • Defmacro-untouchable
            • Add-global-stobj
            • Defthmr
            • Defstub
            • Defrefinement
            • Deflabel
            • In-arithmetic-theory
            • Unmemoize
            • Defabsstobj-missing-events
            • Defthmd
            • Fake-event
            • Set-body
            • Defun-notinline
            • Functions-after
            • Macros-after
            • Dump-events
            • Defund-nx
            • Defun$
            • Remove-global-stobj
            • Remove-custom-keyword-hint
            • Dft
            • Defthy
            • Defund-notinline
            • Defnd
            • Defn
            • Defund-inline
            • Defmacro-last
          • Parallelism
          • History
          • Programming
          • Operational-semantics
          • Real
          • Start-here
          • Miscellaneous
          • Output-controls
          • Bdd
          • Macros
          • Installation
          • Mailing-lists
        • 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))