def Float.Model.UnpackedFloat.packComponents (spec : Format) (sign : Sign) (exponent : BitVec spec.exponentBits) (mantissa : BitVec spec.mantissaBitsWithoutImplicit) : BitVec spec.numBits

Creates a packed float from a sign, an exponent and a mantissa.

def Float.Model.UnpackedFloat.packedInfinity (spec : Format) (sign : Sign) : BitVec spec.numBits

Creates the packed signed infinity representation for the given specification.

def Float.Model.UnpackedFloat.packedNaN (spec : Format) : BitVec spec.numBits

Creates the canonical packed NaN for the given specification.

def Float.Model.UnpackedFloat.packedZero (spec : Format) (sign : Sign) : BitVec spec.numBits

Creates the packed signed zero representation for the given specification.

def Float.Model.UnpackedFloat.pack (spec : Format) : UnpackedFloat → BitVec spec.numBits

Packs the given float into the format given by the specification.

This function assumes that the float is already correctly rounded for the given specification. This means that the exponent must be equal to the exponent computed by spec.targetExponent.

def Float.Model.UnpackedFloat.unpackMantissa {spec : Format} (b : BitVec spec.numBits) : BitVec spec.mantissaBitsWithoutImplicit

Unpacks the mantissa portion of the packed float. If this is a normal number, this will be missing the implicit bit.

def Float.Model.UnpackedFloat.unpackExponent {spec : Format} (b : BitVec spec.numBits) : BitVec spec.exponentBits

Unpacks the exponent portion of the packed float.

def Float.Model.UnpackedFloat.unpackSign {spec : Format} (b : BitVec spec.numBits) : BitVec 1

Unpacks the sign bit of the packed float.

def Float.Model.UnpackedFloat.unpack (spec : Format) (b : BitVec spec.numBits) : UnpackedFloat

Unpacks the given float according to the given specification.

The resulting float may be assumed to be correctly rounded for the given specification.