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
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
List-in
List-notin
Typed-osets
Osets-of-natural-numbers
Osets-of-integer-numbers
Set-all-integerp
Integer-setp
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
Typed-osets
Osets-of-integer-numbers
Finite sets of
integer numbers.
Subtopics
Set-all-integerp
Check if all the elements of a set are integer numbers.
Integer-setp
Recognize finite sets of integer numbers.