• 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
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
        • Atc
        • Language
        • Representation
          • Representation-of-integer-operations
          • Atc-arrays
          • Representation-of-integers
            • Def-integer-values
            • Ushort-list-from-integer-list
            • Ullong-list-from-integer-list
            • Sshort-list-from-integer-list
            • Sllong-list-from-integer-list
            • Integer-list-from-ushort-list
            • Integer-list-from-ullong-list
            • Integer-list-from-sshort-list
            • Integer-list-from-sllong-list
            • Ulong-list-from-integer-list
            • Uchar-list-from-integer-list
            • Slong-list-from-integer-list
            • Schar-list-from-integer-list
            • Integer-list-from-ulong-list
            • Integer-list-from-uchar-list
            • Integer-list-from-slong-list
            • Integer-list-from-schar-list
            • Uint-list-from-integer-list
            • Sint-list-from-integer-list
            • Integer-list-from-uint-list
            • Integer-list-from-sint-list
            • Cinteger
              • Cintegerp
              • Cinteger-fix
              • Cinteger-equiv
              • Cinteger-ushort
              • Cinteger-ulong
              • Cinteger-ullong
              • Cinteger-uint
              • Cinteger-uchar
                • Cinteger-uchar->get
                • Make-cinteger-uchar
                • Change-cinteger-uchar
              • Cinteger-sshort
              • Cinteger-slong
              • Cinteger-sllong
              • Cinteger-sint
              • Cinteger-schar
              • Cinteger-kind
            • Ullongp
            • Ucharp
            • Sintp
            • Ushortp
            • Ulongp
            • Uintp
            • Sllongp
            • Slongp
            • Sshortp
            • Scharp
            • Integer-from-sshort
            • Integer-from-sllong
            • Integer-from-sint
            • Integer-from-slong
            • Integer-from-schar
            • Integer-type-to-fixtype
            • Integer-from-ushort
            • Integer-from-ullong
            • Integer-from-uchar
            • Integer-from-cinteger
            • Integer-from-ulong
            • Integer-from-uint
            • Def-integer-values-loop
            • Sint-from-integer
            • Sint
            • Fixtype-to-integer-type
            • Uchar-from-integer
            • Ushort-from-integer-mod
            • Ushort-from-integer
            • Ulong-from-integer-mod
            • Ulong-from-integer
            • Ullong-from-integer-mod
            • Ullong-from-integer
            • Uchar-from-integer-mod
            • Sshort-from-integer
            • Slong-from-integer
            • Sllong-from-integer
            • Schar-from-integer
            • Uint-from-integer-mod
            • Uint-from-integer
            • Uchar
            • Schar
            • Ushort
            • Ulong
            • Ullong
            • Sshort
            • Slong
            • Sllong
            • Ullong-fix
            • Uint
            • Uchar-fix
            • Sint-fix
            • Ushort-fix
            • Ulong-fix
            • Uint-fix
            • Sshort-fix
            • Slong-fix
            • Sllong-fix
            • Schar-fix
            • Ushort-list
            • Ulong-list
            • Ullong-list
            • Uint-list
            • Uchar-list
            • Sshort-list
            • Slong-list
            • Sllong-list
            • Sint-list
            • Schar-list
            • Integer-type-to/from-fixtype-theorems
            • *nonchar-integer-fixtypes*
          • Representation-of-integer-conversions
          • Pointed-integers
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Cinteger

Cinteger-uchar

This is a product type, introduced by fty::defflexsum in support of cinteger.

Fields

get — ucharp

Subtopics

Cinteger-uchar->get

Get the get field from a cinteger-uchar.

Make-cinteger-uchar

Basic constructor macro for cinteger-uchar structures.

Change-cinteger-uchar

Modifying constructor for cinteger-uchar structures.