• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
        • Pretty-printing
          • Pretty-printing-implementation
          • Eviscerate
            • Eviscconfig
              • Eviscconfig-fix
              • Eviscconfig-equiv
              • Make-eviscconfig
              • Eviscconfig->print-level
              • Eviscconfig->print-length
              • Eviscconfig-p
              • Change-eviscconfig
              • Eviscconfig->replacement-alist
              • Eviscconfig->hiding-cars
            • Eviscerate1
            • Eviscerate1p
          • Pretty
          • Revappend-pretty
          • Pretty-list
        • Printtree
        • Base64
        • Charset-p
        • Strtok!
        • Cases
        • Concatenation
        • Html-encoding
        • Character-kinds
        • Substrings
        • Strtok
        • Equivalences
        • Url-encoding
        • Lines
        • Explode-implode-equalities
        • Ordering
        • Numbers
        • Pad-trim
        • Coercion
        • Std/strings/digit-to-char
        • Substitution
        • Symbols
      • Std/osets
      • Std/io
      • Std/basic
      • Std/system
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
      • Std/typed-alists
      • Std/stobjs
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Eviscerate

Eviscconfig

Controls how to eviscerate a term—our alternative to ACL2's evisc-tuples.

This is a product type introduced by fty::defprod.

Fields
print-level — ACL2::maybe-natp
Similar to the Common Lisp *print-level*. If set, this limits how deeply to descend into subterms before we eviscerate them.
print-length — ACL2::maybe-natp
Similar to the Common lisp *print-length*. If set, this limits how many elements of a list to print (at any level).
replacement-alist
Ordinary (non-fast) alist. Binds subterms either to strings (which are interpreted as the eviscerated replacement text for the subterms) or else to replacement terms (which are not to be recursively eviscerated).
hiding-cars
Should be a fast alist. Binds symbols to T. Any subterm whose car is bound in hiding-cars will be eviscerated with <hidden>.

Subtopics

Eviscconfig-fix
Fixing function for eviscconfig structures.
Eviscconfig-equiv
Basic equivalence relation for eviscconfig structures.
Make-eviscconfig
Basic constructor macro for eviscconfig structures.
Eviscconfig->print-level
Get the print-level field from a eviscconfig.
Eviscconfig->print-length
Get the print-length field from a eviscconfig.
Eviscconfig-p
Recognizer for eviscconfig structures.
Change-eviscconfig
Modifying constructor for eviscconfig structures.
Eviscconfig->replacement-alist
Get the replacement-alist field from a eviscconfig.
Eviscconfig->hiding-cars
Get the hiding-cars field from a eviscconfig.