def Float.Model.UnpackedFloat.roundToInt (sign : Sign) (mantissa : Nat) (exponent : Int) : Int

Returns an Int that is close to the given (sign, mantissa, exponent) triple. Specifically, we round to zero rather than rounding to nearest like we do everywhere else.

Equations

• One or more equations did not get rendered due to their size.

def Float.Model.UnpackedFloat.toInt (negativeInfinity positiveInfinity : Int) : UnpackedFloat → Int

Converts an UnpackedFloat to an Int, sending NaN to 0 and positive and negative infinity to the given values.

Equations

• Float.Model.UnpackedFloat.toInt negativeInfinity positiveInfinity Float.Model.UnpackedFloat.notANumber = 0
• Float.Model.UnpackedFloat.toInt negativeInfinity positiveInfinity (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive) = positiveInfinity
• Float.Model.UnpackedFloat.toInt negativeInfinity positiveInfinity (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative) = negativeInfinity
• Float.Model.UnpackedFloat.toInt negativeInfinity positiveInfinity (Float.Model.UnpackedFloat.zero sign) = 0
• Float.Model.UnpackedFloat.toInt negativeInfinity positiveInfinity (Float.Model.UnpackedFloat.finite s m e mantissa_pos) = Float.Model.UnpackedFloat.roundToInt s m e

def Float.Model.UnpackedFloat.toUInt8 (f : UnpackedFloat) : UInt8

Converts an UnpackedFloat to a UInt8, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toUInt8 = UInt8.ofNatClamp (Float.Model.UnpackedFloat.toInt 0 (↑UInt8.size - 1) f).toNat

def Float.Model.UnpackedFloat.toUInt16 (f : UnpackedFloat) : UInt16

Converts an UnpackedFloat to a UInt16, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toUInt16 = UInt16.ofNatClamp (Float.Model.UnpackedFloat.toInt 0 (↑UInt16.size - 1) f).toNat

def Float.Model.UnpackedFloat.toUInt32 (f : UnpackedFloat) : UInt32

Converts an UnpackedFloat to a UInt32, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toUInt32 = UInt32.ofNatClamp (Float.Model.UnpackedFloat.toInt 0 (↑UInt32.size - 1) f).toNat

def Float.Model.UnpackedFloat.toUInt64 (f : UnpackedFloat) : UInt64

Converts an UnpackedFloat to a UInt64, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toUInt64 = UInt64.ofNatClamp (Float.Model.UnpackedFloat.toInt 0 (↑UInt64.size - 1) f).toNat

def Float.Model.UnpackedFloat.toUSize (f : UnpackedFloat) : USize

Converts an UnpackedFloat to a USize, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toUSize = USize.ofNatClamp (Float.Model.UnpackedFloat.toInt 0 (↑USize.size - 1) f).toNat

def Float.Model.UnpackedFloat.toInt8 (f : UnpackedFloat) : Int8

Converts an UnpackedFloat to an Int8, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toInt8 = Int8.ofIntClamp (Float.Model.UnpackedFloat.toInt Int8.minValue.toInt Int8.maxValue.toInt f)

def Float.Model.UnpackedFloat.toInt16 (f : UnpackedFloat) : Int16

Converts an UnpackedFloat to an Int16, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toInt16 = Int16.ofIntClamp (Float.Model.UnpackedFloat.toInt Int16.minValue.toInt Int16.maxValue.toInt f)

def Float.Model.UnpackedFloat.toInt32 (f : UnpackedFloat) : Int32

Converts an UnpackedFloat to an Int32, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toInt32 = Int32.ofIntClamp (Float.Model.UnpackedFloat.toInt Int32.minValue.toInt Int32.maxValue.toInt f)

def Float.Model.UnpackedFloat.toInt64 (f : UnpackedFloat) : Int64

Converts an UnpackedFloat to an Int64, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toInt64 = Int64.ofIntClamp (Float.Model.UnpackedFloat.toInt Int64.minValue.toInt Int64.maxValue.toInt f)

def Float.Model.UnpackedFloat.toISize (f : UnpackedFloat) : ISize

Converts an UnpackedFloat to an ISize, truncating after the decimal point, sending NaN to 0 and clamping out-of-range values and infinities.

Equations

• f.toISize = ISize.ofIntClamp (Float.Model.UnpackedFloat.toInt ISize.minValue.toInt ISize.maxValue.toInt f)