9.4. Fixed-Precision Integer Types🔗

Planned Content

Compile-time and run-time characteristics for UInt8, UInt16, UInt32, UInt64
Compile-time and run-time characteristics for USize
Compile-time and run-time characteristics for Int8, Int16, Int32, Int64
API reference

Tracked at issue #105

structure

USize : Type

A USize is an unsigned integer with the size of a word for the platform's architecture.

For example, if running on a 32-bit machine, USize is equivalent to UInt32. Or on a 64-bit machine, UInt64.

Constructor

USize.mk
    (toBitVec : BitVec System.Platform.numBits)
    : USize

Fields

`toBitVec`	:	`BitVec System.Platform.numBits`
		Unpack a `USize` as a `BitVec System.Platform.numBits`. This function is overridden with a native implementation.

structure

UInt8 : Type

The type of unsigned 8-bit integers. This type has special support in the compiler to make it actually 8 bits rather than wrapping a Nat.

Constructor

UInt8.mk (toBitVec : BitVec 8) : UInt8

Fields

`toBitVec`	:	`BitVec 8`
		Unpack a `UInt8` as a `BitVec 8`. This function is overridden with a native implementation.

structure

Int8 : Type

The type of signed 8-bit integers. This type has special support in the compiler to make it actually 8 bits rather than wrapping a Nat.

Constructor

Int8.mk (toUInt8 : UInt8) : Int8

Fields

`toUInt8`	:	`UInt8`
		Obtain the `UInt8` that is 2's complement equivalent to the `Int8`.

structure

UInt16 : Type

The type of unsigned 16-bit integers. This type has special support in the compiler to make it actually 16 bits rather than wrapping a Nat.

Constructor

UInt16.mk (toBitVec : BitVec 16) : UInt16

Fields

`toBitVec`	:	`BitVec 16`
		Unpack a `UInt16` as a `BitVec 16`. This function is overridden with a native implementation.

structure

Int16 : Type

The type of signed 16-bit integers. This type has special support in the compiler to make it actually 16 bits rather than wrapping a Nat.

Constructor

Int16.mk (toUInt16 : UInt16) : Int16

Fields

`toUInt16`	:	`UInt16`
		Obtain the `UInt16` that is 2's complement equivalent to the `Int16`.

structure

UInt32 : Type

The type of unsigned 32-bit integers. This type has special support in the compiler to make it actually 32 bits rather than wrapping a Nat.

Constructor

UInt32.mk (toBitVec : BitVec 32) : UInt32

Fields

`toBitVec`	:	`BitVec 32`
		Unpack a `UInt32` as a `BitVec 32. This function is overridden with a native implementation.

structure

Int32 : Type

The type of signed 32-bit integers. This type has special support in the compiler to make it actually 32 bits rather than wrapping a Nat.

Constructor

Int32.mk (toUInt32 : UInt32) : Int32

Fields

`toUInt32`	:	`UInt32`
		Obtain the `UInt32` that is 2's complement equivalent to the `Int32`.

structure

UInt64 : Type

The type of unsigned 64-bit integers. This type has special support in the compiler to make it actually 64 bits rather than wrapping a Nat.

Constructor

UInt64.mk (toBitVec : BitVec 64) : UInt64

Fields

`toBitVec`	:	`BitVec 64`
		Unpack a `UInt64` as a `BitVec 64`. This function is overridden with a native implementation.

structure

Int64 : Type

The type of signed 64-bit integers. This type has special support in the compiler to make it actually 64 bits rather than wrapping a Nat.

Constructor

Int64.mk (toUInt64 : UInt64) : Int64

Fields

`toUInt64`	:	`UInt64`
		Obtain the `UInt64` that is 2's complement equivalent to the `Int64`.