• 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
        • 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
          • Values
            • Integer-values
              • Integer-operations
              • Bit-size
              • Uint
              • Int
            • Boolean-values
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Values

Integer-values

Integer values [SD: Types: Integers].

These are the values of the types uint8 to uint256 and int8 to int256 where the numbers go in increments of 8.

First we introduce a fixtype of the 32 possible sizes of those types, and then we introduce two fixtypes for unsigned and signed integers. The values of the latter two fixtypes carry their own size. These two fixtypes consist of the sets of values of all the the unsigned or signed integer types.

Subtopics

Integer-operations
Integer operations [SD: Types: Integers].
Bit-size
Fixtype of sizes in bits of the integer values.
Uint
Fixtype of unsigned integer values.
Int
Fixtype of signed integer values.