Trait ExecSpecSeqToMultiset 

pub trait ExecSpecSeqToMultiset<'a>: Sized {
    type Elem: DeepView + DeepViewClone + Hash + Eq;

    // Required method
    exec fn exec_to_multiset(self) -> ExecMultiset<Self::Elem>;
}

Spec for executable version of Seq::to_multiset.

Required Associated Types

type Elem: DeepView + DeepViewClone + Hash + Eq

Required Methods

exec fn exec_to_multiset(self) -> ExecMultiset<Self::Elem>

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 + DeepViewClone + Hash + Eq> ExecSpecSeqToMultiset<'a> for &'a [T]

exec fn exec_to_multiset(self) -> res : ExecMultiset<Self::Elem>

ensures

res.deep_view() =~= self.deep_view().to_multiset(),

type Elem = T

Implementors