Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
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
Soft
Bv
Imp-language
Event-macros
C
Java
Atj
Atj-implementation
Atj-types
Atj-java-primitive-array-model
Atj-java-abstract-syntax
Atj-input-processing
Atj-java-pretty-printer
Atj-code-generation
Atj-gen-test-method
Atj-shallow-code-generation
Atj-common-code-generation
Atj-shallow-quoted-constant-generation
Atj-pre-translation
Atj-pre-translation-array-analysis
Atj-pre-translation-type-annotation
Atj-pre-translation-var-reuse
Atj-mark-term
Atj-vars-in-jexpr
Atj-vars-in-jexpr-list
Atj-mark-lambda-formals
Atj-mark-formals+body
Atj-unmark-vars
Atj-unmark-var
Atj-mark-vars-new
Atj-mark-var-new
Atj-mark-var-old
Atj-pre-translate
Atj-pre-translation-multiple-values
Atj-pre-translation-no-aij-types-analysis
Atj-pre-translation-var-renaming
Atj-pre-translation-remove-return-last
Atj-pre-translation-disjunctions
Atj-pre-translation-trivial-vars
Atj-pre-translation-conjunctions
Atj-pre-translation-unused-vars
Atj-pre-translation-remove-dead-if-branches
Atj-gen-everything
Atj-name-translation
Atj-gen-test-cunit
Atj-gen-test-class
Atj-gen-main-file
Atj-post-translation
Atj-deep-code-generation
Atj-gen-test-methods
Atj-gen-test-file
Atj-gen-env-file
Atj-gen-output-subdir
Atj-java-primitives
Atj-java-primitive-arrays
Atj-type-macros
Atj-java-syntax-operations
Atj-fn
Atj-library-extensions
Atj-java-input-types
Atj-test-structures
Aij-notions
Atj-macro-definition
Atj-tutorial
Aij
Language
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Atj-vars-in-jexpr
Atj-vars-in-jexpr-list
Signature
(atj-vars-in-jexpr-list terms) → vars
Arguments
terms
—
Guard
(
pseudo-term-listp
terms)
.
Returns
vars
—
Type
(
symbol-listp
vars)
.