SpecPartialIsoProof

vest_lib::regular::modifier

Trait SpecPartialIsoProof 

Source 
pub trait SpecPartialIsoProof: SpecPartialIsoFn {
    // Required methods
    proof fn spec_iso(s: Self::Src);
    proof fn spec_iso_rev(d: Self::Dst);
}
Expand description

The proof of SpecPartialIsoFn

Required Methods§

Source

proof fn spec_iso(s: Self::Src)

ensures
Self::spec_apply(
    s,
) matches Ok(
    d,
) ==> Self::spec_rev_apply(d) == Ok::<_, <Self::Src as SpecTryFrom<Self::Dst>>::Error>(s),

One direction of the isomorphism when the conversion is successful.

Source

proof fn spec_iso_rev(d: Self::Dst)

ensures
Self::spec_rev_apply(
    d,
) matches Ok(
    s,
) ==> Self::spec_apply(s) == Ok::<_, <Self::Dst as SpecTryFrom<Self::Src>>::Error>(d),

The other direction of the isomorphism when the conversion is successful.

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§