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-pre-translate
Atj-pre-translation-multiple-values
Atj-restore-mv-calls-in-term
Atj-restore-mv-calls-in-args
Atj-restore-mv-calls-in-body
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-restore-mv-calls-in-term
Atj-restore-mv-calls-in-args
Signature
(atj-restore-mv-calls-in-args args wrld) → new-args
Arguments
args
—
Guard
(
pseudo-term-listp
args)
.
wrld
—
Guard
(
plist-worldp
wrld)
.
Returns
new-args
—
Type
(
and
(
pseudo-term-listp
new-args) (
equal
(
len
new-args) (
len
args)))
, given
(
pseudo-term-listp
args)
.