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-shallow-quoted-constant-generation
Atj-qconstants-p
Atj-qconstants
Make-atj-qconstants
Change-atj-qconstants
Honsed-atj-qconstants
Make-honsed-atj-qconstants
Atj-qconstants->symbols
Atj-qconstants->strings
Atj-qconstants->rationals
Atj-qconstants->pairs
Atj-qconstants->numbers
Atj-qconstants->next-index
Atj-qconstants->integers
Atj-qconstants->chars
Atj-gen-shallow-symbol
Atj-gen-shallow-cons-field-name
Atj-gen-shallow-symbol-field-name
Atj-add-qconstant
Atj-add-qconstants-in-term
Atj-gen-shallow-symbol-field
Atj-gen-shallow-rational-id-part
Atj-gen-shallow-number-id-part
Atj-gen-shallow-number-field
Atj-gen-shallow-value
Atj-gen-shallow-cons-fields
Atj-gen-shallow-cons-field
Atj-gen-shallow-string
Atj-gen-shallow-integer-id-part
Atj-gen-shallow-string-field
Atj-gen-shallow-number-field-name
Atj-gen-shallow-char-field
Atj-gen-shallow-char
Atj-gen-shallow-string-field-name
Atj-gen-shallow-cons
Atj-gen-shallow-char-field-name
Atj-gen-shallow-symbol-fields
Atj-gen-shallow-string-fields
Atj-gen-shallow-number-fields
Atj-gen-shallow-number
Atj-gen-shallow-char-fields
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-qconstants-p
Atj-qconstants->next-index
Access the
next-index
field of a
atj-qconstants-p
structure.