Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Abnf
Fty-extensions
Isar
Kestrel-utilities
Omaps
Directed-untranslate
Include-book-paths
Ubi
Digits-any-base
Defdigits
Defdigits-implementation
Defdigits-fn
Defdigits-infop
Defdigits-macro-definition
Defdigits-table
*defdigits-table-name*
Nat=>lendian*
Group-lendian
Defdigit-grouping
Ungroup-lendian
Lendian=>nat
Defthm-dab-return-types
Bendian=>nat
Nat=>bendian*
Trim-bendian*
Trim-lendian*
Nat=>lendian
Dab-digit-list-fix
Nat=>bendian
Ungroup-bendian
Group-bendian
Digits=>nat-injectivity-theorems
Dab-digit-listp
Nat=>lendian+
Dab-basep
Nat=>bendian+
Digits=>nat=>digits-inverses-theorems
Trim-lendian+
Trim-bendian+
Nat=>digits=>nat-inverses-theorems
Dab-digitp
Group/ungroup-inverses-theorems
Dab-digit-fix
Nat=>digits-injectivity-theorems
Dab-base
Digits-any-base-pow2
Dab-base-fix
Context-message-pair
Numbered-names
With-auto-termination
Make-termination-theorem
Theorems-about-true-list-lists
Checkpoint-list
Sublis-expr+
Prove$
Defthm<w
System-utilities-non-built-in
Integer-range-fix
Minimize-ruler-extenders
Integers-from-to
Add-const-to-untranslate-preprocess
Unsigned-byte-fix
Signed-byte-fix
Defthmr
Paired-names
Unsigned-byte-list-fix
Signed-byte-list-fix
Show-books
List-utilities
Skip-in-book
Typed-tuplep
Checkpoint-list-pretty
Defunt
Keyword-value-list-to-alist
Magic-macroexpand
Top-command-number-fn
Bits-as-digits-in-base-2
Show-checkpoint-list
Ubyte11s-as-digits-in-base-2048
Named-formulas
Bytes-as-digits-in-base-256
String-utilities
Make-keyword-value-list-from-keys-and-value
Defmacroq
Integer-range-listp
Apply-fn-if-known
Trans-eval-error-triple
Checkpoint-info-list
Previous-subsumer-hints
Fms!-lst
Zp-listp
Trans-eval-state
Injections
Doublets-to-alist
Theorems-about-osets
Typed-list-utilities
Book-runes-alist
User-interface
Bits/ubyte11s-digit-grouping
Bits/bytes-digit-grouping
Message-utilities
Subsetp-eq-linear
Oset-utilities
Strict-merge-sort-<
Miscellaneous-enumerations
Maybe-unquote
Thm<w
Defthmd<w
Io-utilities
Soft
Bv
Imp-language
Event-macros
C
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Std-extensions
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Defdigits
Defdigits-implementation
Implementation of
defdigits
.
Subtopics
Defdigits-fn
Event generated by
defdigits
.
Defdigits-infop
Information about a successful
defdigits
call, recorded as a pair's value in the
defdigits
table.
Defdigits-macro-definition
Definition of the
defdigits
macro.
Defdigits-table
Table
of successful
defdigits
calls.
*defdigits-table-name*
Name of the
defdigits
table.