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-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
Helpers
Std-extensions
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Atj-code-generation
Atj-common-code-generation
Code generation that is common to the deep and shallow embedding approaches.
Subtopics
Atj-gen-value
Generate Java code to build an ACL2 value.
Atj-chars-to-jhexcodes
Lift
atj-char-to-jhexcode
to lists.
Atj-gen-test-value
Generate the Java code for a test value.
Atj-gen-test-main-method
Generate the Java main method for the test Java class.
Atj-gen-value-flat
Generate flat Java code to build an ACL2 value.
Atj-gen-test-values
Lift
atj-gen-test-value
to lists.
Atj-gen-jlocvar-indexed
Generate a Java declaration for an indexed local variable.
Atj-gen-pkg-method
Generate a Java method that adds an ACL2 package definition.
Atj-gen-symbol
Generate Java code to build an ACL2 symbol.
Atj-gen-jstring
Generate Java code to build a Java string from an ACL2 string.
Atj-gen-init-method
Generate the Java public method to initialize the ACL2 environment.
Atj-gen-char
Generate Java code to build an ACL2 character.
Atj-gen-string
Generate Java code to build an ACL2 string.
Atj-gen-pkg-name
Generate Java code to build an ACL2 package name.
Atj-gen-integer
Generate Java code to build an ACL2 integer.
Atj-gen-test-method-name
Name of the Java method to run one of the specified tests.
Atj-gen-paramlist
Generate a Java formal parameter list from the specified names and Java types.
Atj-gen-pkg-method-name
Name of the Java method that adds an ACL2 package definition.
Atj-gen-run-tests
Generate Java code to run the specified tests.
Atj-gen-jshort-array
Generate Java code to build a Java
short
array.
Atj-gen-jboolean-array
Generate Java code to build a Java
boolean
array.
Atj-gen-test-failures-field
Generate the Java field that keeps track of failures in the test Java class.
Atj-gen-pkgs
Generate Java code to build the ACL2 packages.
Atj-gen-jlong-array
Generate Java code to build a Java
long
array.
Atj-gen-jint-array
Generate Java code to build a Java
int
array.
Atj-gen-jchar-array
Generate Java code to build a Java
char
array.
Atj-gen-jchar
Generate Java code to build a Java
char
from an unsigned 16-bit ACL2 integer.
Atj-gen-jbyte-array
Generate Java code to build a Java
byte
array.
Atj-char-to-jhexcode
Turn an ACL2 character into a Java hexadecimal literal expression corresponding to the character code.
Atj-gen-pkg-methods
Generate all the Java methods that add the ACL2 package definitions.
Atj-gen-number
Generate Java code to build an ACL2 number.
Atj-gen-symbols
Lift
atj-gen-symbol
to lists.
Atj-gen-static-initializer
Generate the static initializer of the main Java class.
Atj-gen-rational
Generate Java code to build an ACL2 rational.
Atj-gen-jlong
Generate Java code to build a Java
long
from a signed 64-bit ACL2 integer.
Atj-gen-jboolean
Generate Java code to build a Java
boolean
from an ACL2 boolean.
Atj-gen-jbigint
Generate Java code to build a Java
BigInteger
from an ACL2 integer.
Atj-gen-jshort
Generate Java code to build a Java
short
from a signed 16-bit signed ACL2 integer.
Atj-gen-jint
Generate Java code to build a Java
int
from a signed 32-bit ACL2 integer.
Atj-gen-jbyte
Generate Java code to build a Java
byte
from a signed 8-bit ACL2 integer.
*atj-gen-pkg-name-alist*