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§
Required Methods§
Sourcespec fn to_bits_spec(&self) -> Self::Bits
spec fn to_bits_spec(&self) -> Self::Bits
Sourcespec fn to_bits_abs_spec(&self) -> Self::Bits
spec fn to_bits_abs_spec(&self) -> Self::Bits
Sourcespec fn is_sign_negative_spec(&self) -> bool
spec fn is_sign_negative_spec(&self) -> bool
Sourcespec fn is_finite_spec(&self) -> bool
spec fn is_finite_spec(&self) -> bool
Sourcespec fn is_infinite_spec(&self) -> bool
spec fn is_infinite_spec(&self) -> bool
Sourcespec fn is_nan_spec(&self) -> bool
spec fn is_nan_spec(&self) -> bool
Implementations on Foreign Types§
Source§impl FloatBitsProperties for f32
impl FloatBitsProperties for f32
Source§open spec fn to_bits_spec(&self) -> u32
open spec fn to_bits_spec(&self) -> u32
{ f32_to_bits(*self) }Source§open spec fn to_bits_abs_spec(&self) -> u32
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 }
}Source§open spec fn is_sign_negative_spec(&self) -> bool
open spec fn is_sign_negative_spec(&self) -> bool
{ self.to_bits_spec() >= 0x8000_0000 }Source§open spec fn is_finite_spec(&self) -> bool
open spec fn is_finite_spec(&self) -> bool
{ self.to_bits_abs_spec() < 0x7f80_0000 }Source§open spec fn is_infinite_spec(&self) -> bool
open spec fn is_infinite_spec(&self) -> bool
{ self.to_bits_abs_spec() == 0x7f80_0000 }Source§open spec fn is_nan_spec(&self) -> bool
open spec fn is_nan_spec(&self) -> bool
{ self.to_bits_abs_spec() > 0x7f80_0000 }type Bits = u32
Source§impl FloatBitsProperties for f64
impl FloatBitsProperties for f64
Source§open spec fn to_bits_spec(&self) -> u64
open spec fn to_bits_spec(&self) -> u64
{ f64_to_bits(*self) }Source§open spec fn to_bits_abs_spec(&self) -> u64
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
}
}Source§open spec fn is_sign_negative_spec(&self) -> bool
open spec fn is_sign_negative_spec(&self) -> bool
{ self.to_bits_spec() >= 0x8000_0000_0000_0000 }Source§open spec fn is_finite_spec(&self) -> bool
open spec fn is_finite_spec(&self) -> bool
{ self.to_bits_abs_spec() < 0x7ff0_0000_0000_0000 }Source§open spec fn is_infinite_spec(&self) -> bool
open spec fn is_infinite_spec(&self) -> bool
{ self.to_bits_abs_spec() == 0x7ff0_0000_0000_0000 }Source§open spec fn is_nan_spec(&self) -> bool
open spec fn is_nan_spec(&self) -> bool
{ self.to_bits_abs_spec() > 0x7ff0_0000_0000_0000 }