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
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-gen-value
Atj-gen-values
Atj-gen-list
Atj-chars-to-jhexcodes
Atj-gen-test-value
Atj-gen-test-main-method
Atj-gen-value-flat
Atj-gen-test-values
Atj-gen-jlocvar-indexed
Atj-gen-pkg-method
Atj-gen-symbol
Atj-gen-jstring
Atj-gen-init-method
Atj-gen-char
Atj-gen-string
Atj-gen-pkg-name
Atj-gen-integer
Atj-gen-test-method-name
Atj-gen-paramlist
Atj-gen-pkg-method-name
Atj-gen-run-tests
Atj-gen-jshort-array
Atj-gen-jboolean-array
Atj-gen-test-failures-field
Atj-gen-pkgs
Atj-gen-jlong-array
Atj-gen-jint-array
Atj-gen-jchar-array
Atj-gen-jchar
Atj-gen-jbyte-array
Atj-char-to-jhexcode
Atj-gen-pkg-methods
Atj-gen-number
Atj-gen-symbols
Atj-gen-static-initializer
Atj-gen-rational
Atj-gen-jlong
Atj-gen-jboolean
Atj-gen-jbigint
Atj-gen-jshort
Atj-gen-jint
Atj-gen-jbyte
*atj-gen-pkg-name-alist*
Atj-shallow-quoted-constant-generation
Atj-pre-translation
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
Std-extensions
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Atj-gen-value
Atj-gen-values
Signature
(atj-gen-values values jvar-value-base jvar-value-index) → (mv block exprs new-jvar-value-index)
Arguments
values
—
Guard
(
true-listp
values)
.
jvar-value-base
—
Guard
(
stringp
jvar-value-base)
.
jvar-value-index
—
Guard
(
posp
jvar-value-index)
.
Returns
block
—
Type
(
jblockp
block)
.
exprs
—
Type
(
and
(
jexpr-listp
exprs) (
equal
(
len
exprs) (
len
values)))
.
new-jvar-value-index
—
Type
(
posp
new-jvar-value-index)
, given
(
posp
jvar-value-index)
.