• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Mutual-recursion
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Loop$-primer
        • Fast-alists
        • Defmacro
        • Defconst
        • Evaluation
        • Guard
          • Verify-guards
          • Mbe
          • Set-guard-checking
          • Ec-call
          • Print-gv
            • Set-print-gv-defaults
            • Guards-and-evaluation
            • Guard-debug
            • Set-check-invariant-risk
            • Guard-evaluation-table
            • The
            • Guard-evaluation-examples-log
            • Guard-miscellany
            • Defthmg
            • Invariant-risk
            • With-guard-checking
            • Guard-holders
            • Guard-formula-utilities
            • Guard-example
            • Set-verify-guards-eagerness
            • Guard-quick-reference
            • Set-register-invariant-risk
            • Guards-for-specification
            • Guard-evaluation-examples-script
            • Guard-introduction
            • Non-exec
            • Set-guard-msg
            • Safe-mode
            • Set-print-gv-defaults
              • Guard-theorem-example
              • With-guard-checking-event
              • With-guard-checking-error-triple
              • Program-only
              • Guard-checking-inhibited
              • Extra-info
            • Equality-variants
            • Compilation
            • Hons
            • ACL2-built-ins
            • System-attachments
            • Developers-guide
            • Advanced-features
            • Set-check-invariant-risk
            • Numbers
            • Irrelevant-formals
            • Efficiency
            • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
            • Redefining-programs
            • Lists
            • Invariant-risk
            • Errors
            • Defabbrev
            • Conses
            • Alists
            • Set-register-invariant-risk
            • Strings
            • Program-wrapper
            • Get-internal-time
            • Basics
            • Packages
            • Defmacro-untouchable
            • Primitive
            • <<
            • Revert-world
            • Set-duplicate-keys-action
            • Unmemoize
            • Symbols
            • Def-list-constructor
            • Easy-simplify-term
            • Defiteration
            • Defopen
            • Sleep
          • Start-here
          • Real
          • Debugging
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Testing-utilities
        • Math
      • 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))