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-type-<=
Atj-function-type
Atj-type-to-jitype
Atj-type
Atj-typep
Atj-type-case
Atj-type-fix
Atj-type-equiv
Atj-type-jprimarr
Atj-type-jprim
Atj-type-ACL2
Atj-type-ACL2->get
Make-atj-type-ACL2
Change-atj-type-ACL2
Atj-type-kind
Atj-function-type-of-min-input-types
Atj-type-top-join
Atj-atype
Atj-type-bottom-meet
Atj-type-bottom-<=
Atj-type-top-<=
Atj-type-top-list-join
Atj-type-bottom-list-<=
Atj-type-top-list-<=
Atj-type-bottom-list-meet
Atj-type-list-<=
Atj-type-to-pred
Atj-maybe-function-type-info
Atj-atype-<=
Atj-maybe-function-type
Atj-maybe-type
Atj-type-to-keyword
Atj-function-type-info
Atj-type-list-join
Atj-type-list-to-type
Atj-type-list-<
Atj-type-list-meet
Atj-type-from-keyword
Atj-function-type-of-min-input-types-aux
Atj-type-<
Atj-type-list-to-type-list-list
Atj-number-of-results
Atj-function-type-info-default
Atj-type-to-pred-gen-mono-thms-2
Atj-get-function-type-info-from-table
Atj-get-function-type-info
Atj-type-to-pred-gen-mono-thms-1
Atj-type-to-pred-gen-mono-thm
Atj-type-meet
Atj-type-to-type-list
Atj-type-list-to-jitype-list
Atj-type-join
Atj-type-of-value
Atj-type-list-to-keyword-list
Atj-type-semilattices
Atj-type-to-pred-gen-mono-thms
Atj-function-type-info->outputs
Atj-function-type-list->outputs
Atj-function-type-list->inputs
Atj-type-list-from-keyword-list
Atj-type-irrelevant
Atj-symbol-type-alist
Atj-type-list
Atj-function-type-list
Atj-type-list-list
Atj-maybe-type-list
Atj-function-type-info-table
*atj-function-type-info-table-name*
Atj-java-primitive-array-model
Atj-java-abstract-syntax
Atj-input-processing
Atj-java-pretty-printer
Atj-code-generation
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-type
Atj-type-ACL2
This is a product type, introduced by
fty::deftagsum
in support of
atj-type
.
Fields
get —
atj-atype
Subtopics
Atj-type-ACL2->get
Get the
get
field from a
atj-type-ACL2
.
Make-atj-type-ACL2
Basic constructor macro for
atj-type-ACL2
structures.
Change-atj-type-ACL2
Modifying constructor for
atj-type-ACL2
structures.