Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Apt
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
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
Taspi
Bitcoin
Des
Ethereum
Sha-2
Yul
C
Zcash
Proof-checker-itp13
Bigmem
Regex
ACL2-programming-language
Json
X86isa
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Paco
Concurrent-programs
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
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)
.