pub trait SpecIsoFn: SpecIso {
// Required methods
spec fn spec_apply(s: Self::Src) -> Self::Dst;
spec fn spec_rev_apply(s: Self::Dst) -> Self::Src;
}Expand description
The bijective functions of SpecIso
Required Methods§
Sourcespec fn spec_apply(s: Self::Src) -> Self::Dst
spec fn spec_apply(s: Self::Src) -> Self::Dst
Applies the isomorphism to the source type.
Sourcespec fn spec_rev_apply(s: Self::Dst) -> Self::Src
spec fn spec_rev_apply(s: Self::Dst) -> Self::Src
Applies the reverse isomorphism 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.