structure Float.Model.Format.Valid (spec : Format) (b : BitVec spec.numBits) : Prop

Predicate asserting that the bit representation of a float is valid according to the given format. By 'valid' we mean that NaN is encoded using the canonical NaN.

• eq_packedNaN : UnpackedFloat.unpackExponent b = -1#spec.exponentBits → UnpackedFloat.unpackMantissa b ≠ 0#spec.mantissaBitsWithoutImplicit → b = UnpackedFloat.packedNaN spec

  If the bit vector encodes a NaN, then it is the canonical NaN.