11.4. Fixed-Precision Integer Types🔗

Planned Content

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

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

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

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

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

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

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

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

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

Fields

toUInt64 : UInt64

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