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-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
Atj-test-value
Atj-test-value-fix
Atj-test-value-case
Atj-test-valuep
Atj-test-value-equiv
Atj-test-value-kind
Atj-test-value-ACL2
Atj-test-value-jshort[]
Atj-test-value-jshort
Atj-test-value-jlong[]
Atj-test-value-jlong
Atj-test-value-jint[]
Atj-test-value-jint
Atj-test-value-jchar[]
Atj-test-value-jchar
Atj-test-value-jchar->get
Make-atj-test-value-jchar
Change-atj-test-value-jchar
Atj-test-value-jbyte[]
Atj-test-value-jbyte
Atj-test-value-jboolean[]
Atj-test-value-jboolean
Atj-test
Atj-test-value-of-type
Atj-test-values-of-types
Atj-test-value-to-type
Atj-test-values-to-types
Atj-test-value-ACL2-list
Atj-test-value-list
Atj-test-list
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-test-value
Atj-test-value-jchar
This is a product type, introduced by
fty::deftagsum
in support of
atj-test-value
.
Fields
get —
char-value
Subtopics
Atj-test-value-jchar->get
Get the
get
field from a
atj-test-value-jchar
.
Make-atj-test-value-jchar
Basic constructor macro for
atj-test-value-jchar
structures.
Change-atj-test-value-jchar
Modifying constructor for
atj-test-value-jchar
structures.