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-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-deep-term-fns
Atj-gen-deep-test-code
Atj-gen-deep-fndef-method
Atj-gen-deep-fnapp
Atj-gen-deep-env-class
Atj-gen-deep-env-cunit
Atj-gen-deep-lambda
Atj-gen-deep-qconst
Atj-gen-deep-main-class
Atj-gen-deep-term
Atj-gen-deep-terms
Atj-gen-deep-build-method
Atj-gen-deep-call-method
Atj-gen-deep-main-cunit
Atj-gen-deep-fndef-method-name
Atj-gen-deep-fndef-methods
Atj-gen-deep-fndefs
Atj-gen-deep-formals
Atj-gen-deep-var
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-code-generation
Atj-deep-code-generation
Code generation that is specific to the deep embedding approach.
Subtopics
Atj-gen-deep-term-fns
Functions to generate Java code to build deeply embedded ACL2 terms.
Atj-gen-deep-test-code
Generate the code of a test method that is specific to the deep embedding approach.
Atj-gen-deep-fndef-method
Generate a Java method that builds a deeply embedded ACL2 function definition.
Atj-gen-deep-fnapp
Generate Java code to build a deeply embedded ACL2 function call.
Atj-gen-deep-env-class
Generate the declaration of the environment Java class, in the deep embedding approach.
Atj-gen-deep-env-cunit
Generate the Java compilation unit with the environment Java class, in the deep embedding approach.
Atj-gen-deep-lambda
Generate Java code to build a deeply embedded ACL2 lambda expression.
Atj-gen-deep-qconst
Generate Java code to build a deeply embedded ACL2 quoted constant.
Atj-gen-deep-main-class
Generate the main (i.e. non-test) Java class declaration, in the deep embedding approach.
Atj-gen-deep-term
Generate Java code to build a deeply embedded ACL2 term.
Atj-gen-deep-terms
Lift
atj-gen-deep-term
to lists.
Atj-gen-deep-build-method
Generate the method to build the ACL2 environment, in the deep embedding approach.
Atj-gen-deep-call-method
Generate the Java method to call ACL2 functions, in the deep embedding approach.
Atj-gen-deep-main-cunit
Generate the main Java compilation unit, in the deep embedding approach.
Atj-gen-deep-fndef-method-name
Name of the Java method that builds a deeply embedded ACL2 function definition.
Atj-gen-deep-fndef-methods
Lift
atj-gen-deep-fndef-method
to lists.
Atj-gen-deep-fndefs
Generate Java code to build the deeply embedded ACL2 function definitions.
Atj-gen-deep-formals
Generate Java code to build a deeply embedded formals parameter list of an ACL2 named function or lambda expression.
Atj-gen-deep-var
Generate Java code to build a deeply embedded ACL2 variable.