Trait FromSpecImpl 

pub trait FromSpecImpl<T>: Sized + From<T> {
    // Required methods
    exec fn obeys_from_spec() -> bool;
    exec fn from_spec(v: T) -> Self;
}

Required Methods

exec fn obeys_from_spec() -> bool

exec fn from_spec(v: T) -> Self

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl FromSpecImpl<i8> for i16

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i8) -> i16

{ v as i16 }

impl FromSpecImpl<i8> for i32

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i8) -> i32

{ v as i32 }

impl FromSpecImpl<i8> for i64

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i8) -> i64

{ v as i64 }

impl FromSpecImpl<i8> for i128

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i8) -> i128

{ v as i128 }

impl FromSpecImpl<i8> for isize

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i8) -> isize

{ v as isize }

impl FromSpecImpl<i16> for i32

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i16) -> i32

{ v as i32 }

impl FromSpecImpl<i16> for i64

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i16) -> i64

{ v as i64 }

impl FromSpecImpl<i16> for i128

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i16) -> i128

{ v as i128 }

impl FromSpecImpl<i16> for isize

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i16) -> isize

{ v as isize }

impl FromSpecImpl<i32> for i64

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i32) -> i64

{ v as i64 }

impl FromSpecImpl<i32> for i128

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i32) -> i128

{ v as i128 }

impl FromSpecImpl<i64> for i128

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: i64) -> i128

{ v as i128 }

impl FromSpecImpl<u8> for u16

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u8) -> u16

{ v as u16 }

impl FromSpecImpl<u8> for u32

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u8) -> u32

{ v as u32 }

impl FromSpecImpl<u8> for u64

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u8) -> u64

{ v as u64 }

impl FromSpecImpl<u8> for u128

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u8) -> u128

{ v as u128 }

impl FromSpecImpl<u8> for usize

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u8) -> usize

{ v as usize }

impl FromSpecImpl<u16> for u32

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u16) -> u32

{ v as u32 }

impl FromSpecImpl<u16> for u64

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u16) -> u64

{ v as u64 }

impl FromSpecImpl<u16> for u128

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u16) -> u128

{ v as u128 }

impl FromSpecImpl<u16> for usize

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u16) -> usize

{ v as usize }

impl FromSpecImpl<u32> for u64

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u32) -> u64

{ v as u64 }

impl FromSpecImpl<u32> for u128

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u32) -> u128

{ v as u128 }

impl FromSpecImpl<u64> for u128

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(v: u64) -> u128

{ v as u128 }

Implementors