Trait FloatBitsProperties 

pub trait FloatBitsProperties {
    type Bits;

    // Required methods
    spec fn to_bits_spec(&self) -> Self::Bits;
    spec fn to_bits_abs_spec(&self) -> Self::Bits;
    spec fn is_sign_negative_spec(&self) -> bool;
    spec fn is_finite_spec(&self) -> bool;
    spec fn is_infinite_spec(&self) -> bool;
    spec fn is_nan_spec(&self) -> bool;
}

Required Associated Types

type Bits

Required Methods

spec fn to_bits_spec(&self) -> Self::Bits

spec fn to_bits_abs_spec(&self) -> Self::Bits

spec fn is_sign_negative_spec(&self) -> bool

spec fn is_finite_spec(&self) -> bool

spec fn is_infinite_spec(&self) -> bool

spec fn is_nan_spec(&self) -> bool

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl FloatBitsProperties for f32

open spec fn to_bits_spec(&self) -> u32

{ f32_to_bits(*self) }

open spec fn to_bits_abs_spec(&self) -> u32

{
    let bits = self.to_bits_spec();
    if bits >= 0x8000_0000 { (bits - 0x8000_0000) as u32 } else { bits }
}

open spec fn is_sign_negative_spec(&self) -> bool

{ self.to_bits_spec() >= 0x8000_0000 }

open spec fn is_finite_spec(&self) -> bool

{ self.to_bits_abs_spec() < 0x7f80_0000 }

open spec fn is_infinite_spec(&self) -> bool

{ self.to_bits_abs_spec() == 0x7f80_0000 }

open spec fn is_nan_spec(&self) -> bool

{ self.to_bits_abs_spec() > 0x7f80_0000 }

type Bits = u32

impl FloatBitsProperties for f64

open spec fn to_bits_spec(&self) -> u64

{ f64_to_bits(*self) }

open spec fn to_bits_abs_spec(&self) -> u64

{
    let bits = self.to_bits_spec();
    if bits >= 0x8000_0000_0000_0000 {
        (bits - 0x8000_0000_0000_0000) as u64
    } else {
        bits
    }
}

open spec fn is_sign_negative_spec(&self) -> bool

{ self.to_bits_spec() >= 0x8000_0000_0000_0000 }

open spec fn is_finite_spec(&self) -> bool

{ self.to_bits_abs_spec() < 0x7ff0_0000_0000_0000 }

open spec fn is_infinite_spec(&self) -> bool

{ self.to_bits_abs_spec() == 0x7ff0_0000_0000_0000 }

open spec fn is_nan_spec(&self) -> bool

{ self.to_bits_abs_spec() > 0x7ff0_0000_0000_0000 }

type Bits = u64

Implementors