SpecIsoProof

vest_lib::regular::modifier

Trait SpecIsoProof 

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

The proof of SpecIsoFn

Required Methods§

Source

proof fn spec_iso(s: Self::Src)

ensures
Self::spec_rev_apply(Self::spec_apply(s)) == s,

One direction of the isomorphism.

Source

proof fn spec_iso_rev(s: Self::Dst)

ensures
Self::spec_apply(Self::spec_rev_apply(s)) == s,

The other direction of the isomorphism.

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§