• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
          • World
          • Io
            • Fmt
            • Msg
            • Cw
            • Set-evisc-tuple
            • Set-iprint
            • Print-control
            • Read-file-into-string
            • Std/io
            • Msgp
            • Printing-to-strings
            • Evisc-tuple
            • Output-controls
            • Observation
            • *standard-co*
            • Ppr-special-syms
            • Standard-oi
            • Standard-co
            • Without-evisc
            • Serialize
            • Output-to-file
            • Fmt-to-comment-window
            • Princ$
            • Character-encoding
            • Open-output-channel!
            • Cw-print-base-radix
            • Set-print-case
            • Set-print-base
            • Print-object$
            • Extend-pathname
            • Print-object$+
            • Fmx-cw
            • Set-print-radix
            • Set-fmt-hard-right-margin
            • File-write-date$
            • Proofs-co
            • Set-print-base-radix
            • Print-base-p
            • *standard-oi*
            • Wof
            • File-length$
            • Fms!-lst
            • Delete-file$
            • *standard-ci*
            • Write-list
            • Trace-co
            • Fmt!
            • Fms
            • Cw!
            • Fmt-to-comment-window!
            • Fms!
            • Eviscerate-hide-terms
              • Fmt1!
              • Fmt-to-comment-window!+
              • Read-file-into-byte-array-stobj
              • Fmt1
              • Fmt-to-comment-window+
              • Cw-print-base-radix!
              • Read-file-into-character-array-stobj
              • Fmx
              • Cw!+
              • Read-objects-from-book
              • Newline
              • Cw+
              • Probe-file
              • Write-objects-to-file!
              • Write-objects-to-file
              • Read-objects-from-file
              • Read-object-from-file
              • Read-file-into-byte-list
              • Set-fmt-soft-right-margin
              • Read-file-into-character-list
              • Io-utilities
            • Wormhole
            • Programming-with-state
            • W
            • Set-state-ok
            • Random$
          • Mutual-recursion
          • Memoize
          • Mbe
          • Io
            • Fmt
            • Msg
            • Cw
            • Set-evisc-tuple
            • Set-iprint
            • Print-control
            • Read-file-into-string
            • Std/io
            • Msgp
            • Printing-to-strings
            • Evisc-tuple
            • Output-controls
            • Observation
            • *standard-co*
            • Ppr-special-syms
            • Standard-oi
            • Standard-co
            • Without-evisc
            • Serialize
            • Output-to-file
            • Fmt-to-comment-window
            • Princ$
            • Character-encoding
            • Open-output-channel!
            • Cw-print-base-radix
            • Set-print-case
            • Set-print-base
            • Print-object$
            • Extend-pathname
            • Print-object$+
            • Fmx-cw
            • Set-print-radix
            • Set-fmt-hard-right-margin
            • File-write-date$
            • Proofs-co
            • Set-print-base-radix
            • Print-base-p
            • *standard-oi*
            • Wof
            • File-length$
            • Fms!-lst
            • Delete-file$
            • *standard-ci*
            • Write-list
            • Trace-co
            • Fmt!
            • Fms
            • Cw!
            • Fmt-to-comment-window!
            • Fms!
            • Eviscerate-hide-terms
              • Fmt1!
              • Fmt-to-comment-window!+
              • Read-file-into-byte-array-stobj
              • Fmt1
              • Fmt-to-comment-window+
              • Cw-print-base-radix!
              • Read-file-into-character-array-stobj
              • Fmx
              • Cw!+
              • Read-objects-from-book
              • Newline
              • Cw+
              • Probe-file
              • Write-objects-to-file!
              • Write-objects-to-file
              • Read-objects-from-file
              • Read-object-from-file
              • Read-file-into-byte-list
              • Set-fmt-soft-right-margin
              • Read-file-into-character-list
              • Io-utilities
            • Defpkg
            • Apply$
            • Loop$
            • Programming-with-state
            • Arrays
            • Characters
            • Time$
            • Defmacro
            • Loop$-primer
            • Fast-alists
            • Defconst
            • Evaluation
            • Guard
            • Equality-variants
            • Compilation
            • Hons
            • ACL2-built-ins
            • Developers-guide
            • System-attachments
            • Advanced-features
            • Set-check-invariant-risk
            • Numbers
            • Efficiency
            • Irrelevant-formals
            • 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
            • Oracle-eval
            • Defmacro-untouchable
            • <<
            • Primitive
            • Revert-world
            • Unmemoize
            • Set-duplicate-keys-action
            • Symbols
            • Def-list-constructor
            • Easy-simplify-term
            • Defiteration
            • Fake-oracle-eval
            • Defopen
            • Sleep
          • Operational-semantics
          • Real
          • Start-here
          • Debugging
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Io

      Eviscerate-hide-terms

      To print (hide ...) as <hidden>

      Example:
      (assign eviscerate-hide-terms t)
      (assign eviscerate-hide-terms nil)

      Eviscerate-hide-terms is a state global variable whose value is either t or nil. The variable affects how terms are displayed by default (but not if you have set the term-evisc-tuple to other than its default; see set-evisc-tuple). If t, terms of the form (hide ...) are printed as <hidden>. Otherwise, they are printed normally.