Trait ExecSpecSeqIsSuffixOf 

pub trait ExecSpecSeqIsSuffixOf<'a>: DeepView + Sized {
    type Other: DeepView<V = Self::V>;

    // Required method
    exec fn exec_is_suffix_of(self, other: Self::Other) -> res : bool;
}

Spec for executable version of Seq::is_suffix_of.

Required Associated Types

type Other: DeepView<V = Self::V>

Required Methods

exec fn exec_is_suffix_of(self, other: Self::Other) -> res : bool

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl<'a, T: DeepView> ExecSpecSeqIsSuffixOf<'a> for &'a [T]

where &'a T: ExecSpecEq<'a, Other = &'a T>, &'a [T]: DeepView<V = Seq<<&'a T as DeepView>::V>>,

exec fn exec_is_suffix_of(self, other: Self::Other) -> res : bool

ensures

res == self.deep_view().is_suffix_of(other.deep_view()),

type Other = &'a [T]

Implementors