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
Context-message-pair
Numbered-names
Check-numbered-name
Next-numbered-name
Resolve-numbered-name-wildcard
Set-numbered-name-index
Next-fresh-numbered-names
Global-numbered-name-index
Make-numbered-name
Make-numbered-name-list
Set-numbered-name-index-to-global
Numbered-names-in-use
Next-fresh-numbered-name
Numbered-name-index-wildcard
Numbered-name-index-start
Get-numbered-name-index-start
Numbered-name-index-start-p
Set-numbered-name-index-start
*default-numbered-name-index-start*
Numbered-name-index-end
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
Numbered-names
Numbered-name-index-start
Starting marker of the numeric index of numbered names.
This is stored in a singleton
table
.
Subtopics
Get-numbered-name-index-start
Retrieve the current starting marker of the numeric index of numbered names.
Numbered-name-index-start-p
Recognize admissible starting markers of the numeric index of numbered names.
Set-numbered-name-index-start
Set the starting marker of the numeric index of numbered names.
*default-numbered-name-index-start*
Default starting marker of the numeric index of numbered names.