PartialIsoFn

vest_lib::regular::modifier

Trait PartialIsoFn 

Source 
pub trait PartialIsoFn<'x>: PartialIso<'x>
where
    Self::V: SpecPartialIso<Src = <Self::Src as View>::V, Dst = <Self::Dst as View>::V>,
    <Self::Src as View>::V: SpecTryFrom<<Self::Dst as View>::V>,
    <Self::Dst as View>::V: SpecTryFrom<<Self::Src as View>::V>,
    Self::Dst: 'x,
{
    // Required methods
    exec fn apply(
        s: Self::Src,
    ) -> res : Result<Self::Dst, <Self::Dst as TryFrom<Self::Src>>::Error>;
    exec fn rev_apply(
        s: &'x Self::Dst,
    ) -> res : Result<Self::RefSrc, <Self::RefSrc as TryFrom<&'x Self::Dst>>::Error>;
}
Expand description

The fallible functions of PartialIso

Required Methods§

Source

exec fn apply( s: Self::Src, ) -> res : Result<Self::Dst, <Self::Dst as TryFrom<Self::Src>>::Error>

ensures
res matches Ok(
    v,
) ==> {
    &&& Self::V::spec_apply(s@) is Ok
    &&& Self::V::spec_apply(s@) matches Ok(v_) && v@ == v_

},
res matches Err(e) ==> Self::V::spec_apply(s@) is Err,

Applies the fallible conversion to the source type.

Source

exec fn rev_apply( s: &'x Self::Dst, ) -> res : Result<Self::RefSrc, <Self::RefSrc as TryFrom<&'x Self::Dst>>::Error>

ensures
res matches Ok(
    v,
) ==> {
    &&& Self::V::spec_rev_apply(s@) is Ok
    &&& Self::V::spec_rev_apply(s@) matches Ok(v_) && v@ == v_

},
res matches Err(e) ==> Self::V::spec_rev_apply(s@) is Err,

Applies the reverse fallible conversion to the destination type.

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.

Implementors§

Source§

impl<'x, T: PartialIso<'x>> PartialIsoFn<'x> for T
where T::V: SpecPartialIso<Src = <T::Src as View>::V, Dst = <T::Dst as View>::V>, <T::Src as View>::V: SpecTryFrom<<T::Dst as View>::V>, <T::Dst as View>::V: SpecTryFrom<<T::Src as View>::V>, Self::Dst: 'x,