Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Std/lists
Std/alists
Obags
Std/util
Std/strings
Pretty-printing
Pretty-printing-implementation
Eviscerate
Eviscconfig
Eviscerate1
Eviscerate1-lst
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/io
Std/osets
Std/basic
Std/system
Std/typed-lists
Std/bitsets
Std/testing
Std/typed-alists
Std/stobjs
Std-extensions
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Eviscerate1
Eviscerate1-lst
Signature
(eviscerate1-lst x v n config) → *
Arguments
x
— List of objects to eviscerate, including its car.
v
— Depth we are currently at.
Guard
(
natp
v)
.
n
— Length we are currently at.
Guard
(
natp
n)
.
config
—
Guard
(
eviscconfig-p
config)
.