def Float.Model.UnpackedFloat.isNaNBits {spec : Format} (b : BitVec spec.numBits) : Bool

Returns true if the bits represent an NaN value

Equations

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

@[simp]

theorem Float.Model.UnpackedFloat.Sign.ofBitVec_toBitVec (s : Sign) : ofBitVec s.toBitVec = s

@[simp]

theorem Float.Model.UnpackedFloat.Sign.toBitVec_ofBitVec (b : BitVec 1) : (ofBitVec b).toBitVec = b

theorem Float.Model.UnpackedFloat.Sign.forall_iff {p : Sign → Prop} : (∀ (s : Sign), p s) ↔ p positive ∧ p negative

@[instance_reducible]

instance Float.Model.UnpackedFloat.Sign.instDecidableForall_batteries {p : Sign → Prop} [(s : Sign) → Decidable (p s)] : Decidable (∀ (s : Sign), p s)

Equations

• Float.Model.UnpackedFloat.Sign.instDecidableForall_batteries = decidable_of_decidable_of_iff ⋯

instance Float.Model.UnpackedFloat.Sign.instReflBEq_batteries : ReflBEq Sign

instance Float.Model.UnpackedFloat.Sign.instLawfulBEq_batteries : LawfulBEq Sign

theorem Float.Model.UnpackedFloat.unpackMantissa_def {spec : Format} (b : BitVec spec.numBits) : unpackMantissa b = BitVec.extractLsb' 0 spec.mantissaBitsWithoutImplicit b

theorem Float.Model.UnpackedFloat.unpackExponent_def {spec : Format} (b : BitVec spec.numBits) : unpackExponent b = BitVec.extractLsb' spec.mantissaBitsWithoutImplicit spec.exponentBits b

theorem Float.Model.UnpackedFloat.unpackSign_def {spec : Format} (b : BitVec spec.numBits) : unpackSign b = BitVec.extractLsb' (spec.mantissaBitsWithoutImplicit + spec.exponentBits) 1 b

@[simp]

theorem Float.Model.UnpackedFloat.unpackSign_packComponents {spec : Format} (s : Sign) (e : BitVec spec.exponentBits) (m : BitVec spec.mantissaBitsWithoutImplicit) : unpackSign (packComponents spec s e m) = s.toBitVec

theorem Float.Model.UnpackedFloat.packComponents_unpackSign_unpackExponent_unpackMantissa {spec : Format} (b : BitVec spec.numBits) : packComponents spec (Sign.ofBitVec (unpackSign b)) (unpackExponent b) (unpackMantissa b) = b

theorem Float.Model.UnpackedFloat.pack_unpack {spec : Format} (b : BitVec spec.numBits) (hspec : 2 ≤ spec.exponentBits := by decide) : pack spec (unpack spec b) = if isNaNBits b = true then packedNaN spec else b

theorem Float.Model.UnpackedFloat.pack_unpack_of_valid {spec : Format} {b : BitVec spec.numBits} (hvalid : spec.Valid b) (hspec : 2 ≤ spec.exponentBits := by decide) : pack spec (unpack spec b) = b

theorem Float.Model.UnpackedFloat.unpack_inj_of_valid {spec : Format} {b b' : BitVec spec.numBits} (hb : spec.Valid b) (hb' : spec.Valid b') (hspec : 2 ≤ spec.exponentBits := by decide) : unpack spec b = unpack spec b' ↔ b = b'

theorem Float.Model.UnpackedFloat.isNaNBits_packedNaN {spec : Format} : isNaNBits (packedNaN spec) = true

@[simp]

theorem Float.Model.UnpackedFloat.unpack_packedNaN {spec : Format} : unpack spec (packedNaN spec) = notANumber

@[simp]

theorem Float.Model.UnpackedFloat.unpack_packedZero {spec : Format} {sign : Sign} : unpack spec (packedZero spec sign) = zero sign

@[simp]

theorem Float.Model.UnpackedFloat.isNaN_iff {x : UnpackedFloat} : x.isNaN = true ↔ x = notANumber

theorem Float.Model.UnpackedFloat.unpack_eq_notANumber_iff_of_valid {spec : Format} {b : BitVec spec.numBits} (hvalid : spec.Valid b) (hspec : 2 ≤ spec.exponentBits := by decide) : unpack spec b = notANumber ↔ b = packedNaN spec

theorem Float.Model.UnpackedFloat.unpack_eq_zero_iff_of_valid {spec : Format} {sign : Sign} {b : BitVec spec.numBits} (hvalid : spec.Valid b) (hspec : 2 ≤ spec.exponentBits := by decide) : unpack spec b = zero sign ↔ b = packedZero spec sign

theorem Float.Model.UnpackedFloat.isNaN_unpack_iff_of_valid {spec : Format} {b : BitVec spec.numBits} (hvalid : spec.Valid b) (hspec : 2 ≤ spec.exponentBits := by decide) : (unpack spec b).isNaN = true ↔ b = packedNaN spec

theorem Float.Model.UnpackedFloat.beq_iff_ne_notANumber_and_eq (a b : UnpackedFloat) : a.beq b = true ↔ a ≠ notANumber ∧ b ≠ notANumber ∧ (a = b ∨ a = zero Sign.positive ∧ b = zero Sign.negative ∨ a = zero Sign.negative ∧ b = zero Sign.positive)

theorem Float.Model.UnpackedFloat.unpack_beq_unpack_iff {spec : Format} {b b' : BitVec spec.numBits} (hb : spec.Valid b) (hb' : spec.Valid b') (hspec : 2 ≤ spec.exponentBits := by decide) : (unpack spec b).beq (unpack spec b') = true ↔ b ≠ packedNaN spec ∧ b' ≠ packedNaN spec ∧ (b = b' ∨ b = packedZero spec Sign.positive ∧ b' = packedZero spec Sign.negative ∨ b = packedZero spec Sign.negative ∧ b' = packedZero spec Sign.positive)

theorem Float.toBits_inj {f f' : Float} : f.toBits = f'.toBits ↔ f = f'

theorem Float32.toBits_inj {f f' : Float32} : f.toBits = f'.toBits ↔ f = f'

@[simp]

theorem Float.ofBits_toBits (f : Float) : ofBits f.toBits = f

@[simp]

theorem Float32.ofBits_toBits (f : Float32) : ofBits f.toBits = f

@[simp]

theorem Float.isNaN_eq_decide_eq_nan {f : Float} : f.isNaN = decide (f = nan)

@[simp]

theorem Float32.isNaN_eq_decide_eq_nan {f : Float32} : f.isNaN = decide (f = nan)

theorem Float.beq_iff_ne_nan_and_eq {f f' : Float} : (f == f') = true ↔ f ≠ nan ∧ f' ≠ nan ∧ (f = f' ∨ f = 0 ∧ f' = -0 ∨ f = -0 ∧ f' = 0)

theorem Float32.beq_iff_ne_nan_and_eq {f f' : Float32} : (f == f') = true ↔ f ≠ nan ∧ f' ≠ nan ∧ (f = f' ∨ f = 0 ∧ f' = -0 ∨ f = -0 ∧ f' = 0)

@[simp]

theorem Float.nan_beq_eq_false (f : Float) : (nan == f) = false

@[simp]

theorem Float32.nan_beq_eq_false (f : Float32) : (nan == f) = false

@[simp]

theorem Float.beq_nan_eq_false (f : Float) : (f == nan) = false

@[simp]

theorem Float32.beq_nan_eq_false (f : Float32) : (f == nan) = false

@[simp]

theorem Float.beq_self_iff {f : Float} : (f == f) = true ↔ f ≠ nan

@[simp]

theorem Float32.beq_self_iff {f : Float32} : (f == f) = true ↔ f ≠ nan

@[simp]

theorem Float.beq_self_eq_false_iff {f : Float} : (f == f) = false ↔ f = nan

@[simp]

theorem Float32.beq_self_eq_false_iff {f : Float32} : (f == f) = false ↔ f = nan

@[simp]

theorem Float.bne_eq {f : Float} : (f != f) = !f == f

This theorem is true for all types but most other types have LawfulBEq where bne_self_eq_false or bne_iff_ne apply.

@[simp]

theorem Float32.bne_eq {f : Float32} : (f != f) = !f == f

This theorem is true for all types but most other types have LawfulBEq where bne_self_eq_false or bne_iff_ne apply.

instance instPartialEquivBEqFloat_batteries : PartialEquivBEq Float

Boolean equality on Floats is symmetric and transitive, but not reflexive, as demonstrated by nan != nan.

instance instPartialEquivBEqFloat32_batteries : PartialEquivBEq Float32

Boolean equality on Float32s is symmetric and transitive, but not reflexive, as demonstrated by nan != nan.