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
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-jprimarr->comp
Make-atj-type-jprimarr
Change-atj-type-jprimarr
Atj-type-jprim
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
Taspi
Bitcoin
Des
Ethereum
Sha-2
Yul
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-type
Atj-type-jprimarr
This is a product type, introduced by
fty::deftagsum
in support of
atj-type
.
Fields
comp —
primitive-type
Subtopics
Atj-type-jprimarr->comp
Get the
comp
field from a
atj-type-jprimarr
.
Make-atj-type-jprimarr
Basic constructor macro for
atj-type-jprimarr
structures.
Change-atj-type-jprimarr
Modifying constructor for
atj-type-jprimarr
structures.