Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Std/lists
Std/alists
Obags
Std/util
Std/strings
Std/io
Std/osets
Std/basic
Std/system
Std/typed-lists
Std/typed-lists/character-listp
Std/typed-lists/symbol-listp
Std/typed-lists/boolean-listp
Std/typed-lists/string-listp
Std/typed-lists/eqlable-listp
Theorems-about-true-list-lists
Std/typed-lists/atom-listp
Unsigned-byte-listp
Defbytelist
Defbytelist-standard-instances
Defbytelist-implementation
Defbytelist-fn
Defbytelist-macro-definition
Unsigned-byte-list-fix
Cons-listp
Cons-list-listp
Signed-byte-listp
String-or-symbol-listp
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
Defbytelist
Defbytelist-implementation
Implementation of
defbytelist
.
Subtopics
Defbytelist-fn
Events generated by
defbytelist
.
Defbytelist-macro-definition
Definition of the
defbytelist
macro.