• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • C
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
              • Atj-types
                • Atj-type-<=
                • Atj-function-type
                • Atj-type-to-jitype
                • Atj-type
                • Atj-function-type-of-min-input-types
                • Atj-type-top-join
                • Atj-atype
                  • Atj-atype-case
                  • Atj-atype-fix
                  • Atj-atype-equiv
                  • Atj-atypep
                  • Atj-atype-kind
                  • Atj-atype-value
                  • Atj-atype-symbol
                  • Atj-atype-string
                  • Atj-atype-rational
                  • Atj-atype-number
                  • Atj-atype-integer
                  • Atj-atype-cons
                  • Atj-atype-character
                    • Make-atj-atype-character
                    • Change-atj-atype-character
                  • Atj-atype-boolean
                • 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
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Atj-atype

Atj-atype-character

This is a product type, introduced by fty::deftagsum in support of atj-atype.

This is an atomic/empty structure; it has no fields.

Subtopics

Make-atj-atype-character
Basic constructor macro for atj-atype-character structures.
Change-atj-atype-character
Modifying constructor for atj-atype-character structures.