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
Pretty-printing
Printtree
Base64
Charset-p
Strtok!
Cases
Concatenation
Html-encoding
Character-kinds
Substrings
Strtok
Equivalences
Url-encoding
Lines
Explode-implode-equalities
Ordering
Numbers
Decimal
Hex
Parse-hex-from-string
Hex-digit-char-p
Hex-digit-char
Hex-digit-char-fix
Hex-digit-char-list
Hex-digit-char-list-fix
Hex-digit-char-list-equiv
Nat-to-hex-chars
Parse-hex-from-charlist
Hex-digit-chars-value
Hex-digit-char-value
Take-leading-hex-digit-chars
Hexify
Hex-digit-char-list*p
Hex-digit-char-listp
Hex-digit-string-p
Strval16
Skip-leading-hex-digits
Nat-to-hex-string
Hexify-width
Nonzero-hex-digit-char-p
Nat-to-hex-string-list
Revappend-nat-to-hex-chars
Hex-digit-to-char
Nat-to-hex-string-size
Octal
Binary
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
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Fty-extensions
Specific-types
Hex-digit-char
Hex-digit-char-list
Fixtype of lists of hexadecimal digit characters.
This is an ordinary
fty::deflist
.
Subtopics
Hex-digit-char-list-fix
(hex-digit-char-list-fix x)
is a usual
ACL2::fty
list fixing function.
Hex-digit-char-list-equiv
Basic equivalence relation for
hex-digit-char-list
structures.