Search-engine friendly clone of the
ACL2 documentation
.
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
Mutual-recursion
Memoize
Mbe
Io
Defpkg
Apply$
Loop$
Programming-with-state
Arrays
Characters
Time$
Loop$-primer
Fast-alists
Defconst
Defmacro
Evaluation
Guard
Equality-variants
Compilation
Hons
ACL2-built-ins
Developers-guide
System-attachments
Advanced-features
Set-check-invariant-risk
Numbers
Irrelevant-formals
Efficiency
Introduction-to-programming-in-ACL2-for-those-who-know-lisp
Redefining-programs
Lists
Invariant-risk
Errors
Defabbrev
Conses
Alists
Set-register-invariant-risk
Strings
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
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
String-listp
Stringp
Length
Search
Remove-duplicates
Position
Coerce
Concatenate
Reverse
String
Subseq
Substitute
String-upcase
String-downcase
Count
Char
String<
String-equal
String-utilities
String-append
String>=
String<=
String>
Hex-digit-char-theorems
String-downcase-gen
String-upcase-gen
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
Numbers
Hex
Functions for working with hexadecimal numbers in strings.
Subtopics
Parse-hex-from-string
Parse a hexadecimal number from a string, at some offset.
Hex-digit-char-p
Recognizer for hexadecimal digit characters: 0-9, A-F, a-f.
Nat-to-hex-chars
Convert a natural number into a list of hexadecimal bits.
Parse-hex-from-charlist
Parse a hexadecimal number from the beginning of a character list.
Hex-digit-chars-value
Coerces a
hex-digit-char-list*p
into a natural number.
Hex-digit-char-value
Coerces a
hex-digit-char-p
character into a number.
Take-leading-hex-digit-chars
Collect any leading hex digit characters from the start of a character list.
Hexify
Convert numbers into readable hex strings.
Hex-digit-char-list*p
Recognizes lists of
hex-digit-char-p
characters.
Hex-digit-char-listp
Recognize lists of hexadecimal digit characters.
Hex-digit-string-p
Recognizer for strings whose characters are hexadecimal digits.
Strval16
Interpret a string as a hexadecimal number.
Skip-leading-hex-digits
Skip over any leading hex digit characters at the start of a character list.
Nat-to-hex-string
Convert a natural number into a string with its hex digits.
Hexify-width
Convert numbers into readable hex strings, fixing the number of digits printed
Nonzero-hex-digit-char-p
Recognizer for non-zero hexadecimal digit characters: 1-9, A-F, a-f.
Nat-to-hex-string-list
Convert a list of natural numbers into a list of hex digit strings.
Revappend-nat-to-hex-chars
More efficient version of
(
revappend
(
nat-to-hex-chars
n) acc).
Hex-digit-to-char
Convert a number from 0-15 into a hex character.
Nat-to-hex-string-size
Number of characters in the hexadecimal representation of a natural.