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
Printtree
Base64
Charset-p
Strtok!
Cases
Concatenation
Html-encoding
Character-kinds
Substrings
Strtok
Equivalences
Url-encoding
Lines
Explode-implode-equalities
Ordering
Numbers
Decimal
Hex
Octal
Parse-octal-from-string
Parse-octal-from-charlist
Nat-to-oct-chars
Oct-digit-chars-value
Oct-digit-char-p
Oct-digit-char
Oct-digit-char-fix
Oct-digit-char-list
Oct-digit-char-list-fix
Oct-digit-char-list-equiv
Take-leading-oct-digit-chars
Oct-digit-char-value
Oct-digit-char-list*p
Oct-digit-char-listp
Skip-leading-octal-digits
Oct-digit-string-p
Nat-to-oct-string
Strval8
Nat-to-oct-string-list
Revappend-nat-to-oct-chars
Nonzero-oct-digit-char-p
Nat-to-oct-string-size
Octal-digit-to-char
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
Oct-digit-char
Oct-digit-char-list
Fixtype of lists of octal digit characters.
This is an ordinary
fty::deflist
.
Subtopics
Oct-digit-char-list-fix
(oct-digit-char-list-fix x)
is a usual
ACL2::fty
list fixing function.
Oct-digit-char-list-equiv
Basic equivalence relation for
oct-digit-char-list
structures.