• 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
        • Set
        • Soft
        • 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-sshort
                • Cinteger-slong
                • Cinteger-sllong
                • Cinteger-sint
                • Cinteger-schar
                • Cinteger-kind
              • Sintp
              • Ullongp
              • Ucharp
              • 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
            • Shallow-deep-embedding-relation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Representation-of-integers

Cinteger

Fixtype of all the supported C integer types.

This is a sum-of-products (i.e., union) type, introduced by fty::defflexsum.

Members
:schar → cinteger-schar
:uchar → cinteger-uchar
:sshort → cinteger-sshort
:ushort → cinteger-ushort
:sint → cinteger-sint
:uint → cinteger-uint
:slong → cinteger-slong
:ulong → cinteger-ulong
:sllong → cinteger-sllong
:ullong → cinteger-ullong

This is the union of the C integer types listed in *nonchar-integer-fixtypes*.

Subtopics

Cintegerp
Recognizer for cinteger structures.
Cinteger-fix
Fixing function for cinteger structures.
Cinteger-equiv
Basic equivalence relation for cinteger structures.
Cinteger-ushort
Cinteger-ulong
Cinteger-ullong
Cinteger-uint
Cinteger-uchar
Cinteger-sshort
Cinteger-slong
Cinteger-sllong
Cinteger-sint
Cinteger-schar
Cinteger-kind
Get the kind (tag) of a cinteger structure.