These are only the lemmas required to write down the operations on Float.Model and Float32.Model. There will not be any additional lemmas; see the docstring of UnpackedFloat for more details.

@[simp]

theorem Float.Model.UnpackedFloat.unpackMantissa_packComponents {spec : Format} {sign : Sign} {exponent : BitVec spec.exponentBits} {mantissa : BitVec spec.mantissaBitsWithoutImplicit} : unpackMantissa (packComponents spec sign exponent mantissa) = mantissa

@[simp]

theorem Float.Model.UnpackedFloat.unpackExponent_packComponents {spec : Format} {sign : Sign} {exponent : BitVec spec.exponentBits} {mantissa : BitVec spec.mantissaBitsWithoutImplicit} : unpackExponent (packComponents spec sign exponent mantissa) = exponent

@[simp]

theorem Float.Model.UnpackedFloat.valid_pack {spec : Format} {f : UnpackedFloat} : spec.Valid (pack spec f)