Trait NegSpecImpl

Source
pub trait NegSpecImpl: Neg {
    // Required methods
    exec fn obeys_neg_spec() -> bool;
    exec fn neg_req(self) -> bool
       where Self: Sized;
    exec fn neg_spec(self) -> Self::Output
       where Self: Sized;
}

Required Methods§

Source

exec fn obeys_neg_spec() -> bool

Source

exec fn neg_req(self) -> bool
where Self: Sized,

Source

exec fn neg_spec(self) -> Self::Output
where Self: Sized,

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types§

Source§

impl NegSpecImpl for i8

Source§

open spec fn obeys_neg_spec() -> bool

{ true }
Source§

open spec fn neg_req(self) -> bool

{ (-self) as i8 == (-self) }
Source§

open spec fn neg_spec(self) -> Self::Output

{ (-self) as i8 }
Source§

impl NegSpecImpl for i16

Source§

open spec fn obeys_neg_spec() -> bool

{ true }
Source§

open spec fn neg_req(self) -> bool

{ (-self) as i16 == (-self) }
Source§

open spec fn neg_spec(self) -> Self::Output

{ (-self) as i16 }
Source§

impl NegSpecImpl for i32

Source§

open spec fn obeys_neg_spec() -> bool

{ true }
Source§

open spec fn neg_req(self) -> bool

{ (-self) as i32 == (-self) }
Source§

open spec fn neg_spec(self) -> Self::Output

{ (-self) as i32 }
Source§

impl NegSpecImpl for i64

Source§

open spec fn obeys_neg_spec() -> bool

{ true }
Source§

open spec fn neg_req(self) -> bool

{ (-self) as i64 == (-self) }
Source§

open spec fn neg_spec(self) -> Self::Output

{ (-self) as i64 }
Source§

impl NegSpecImpl for i128

Source§

open spec fn obeys_neg_spec() -> bool

{ true }
Source§

open spec fn neg_req(self) -> bool

{ (-self) as i128 == (-self) }
Source§

open spec fn neg_spec(self) -> Self::Output

{ (-self) as i128 }
Source§

impl NegSpecImpl for isize

Source§

open spec fn obeys_neg_spec() -> bool

{ true }
Source§

open spec fn neg_req(self) -> bool

{ (-self) as isize == (-self) }
Source§

open spec fn neg_spec(self) -> Self::Output

{ (-self) as isize }

Implementors§