pub struct ExDefaultHasher(/* private fields */);Expand description
Specifications for the behavior of
std::collections::hash_map::DefaultHasher.
We model a DefaultHasher as having a view (i.e., an abstract
state) of type Seq<Seq<u8>>. This reflects the sequence of write
operations performed so far, where each write is modeled as having
written a sequence of bytes. There’s also a specification for
how a view will be transformed by finish into a u64.
Auto Trait Implementations§
impl Freeze for ExDefaultHasher
impl RefUnwindSafe for ExDefaultHasher
impl Send for ExDefaultHasher
impl Sync for ExDefaultHasher
impl Unpin for ExDefaultHasher
impl UnsafeUnpin for ExDefaultHasher
impl UnwindSafe for ExDefaultHasher
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T, U> IntoSpecImpl<U> for Twhere
U: From<T>,
impl<T, U> IntoSpecImpl<U> for Twhere
U: From<T>,
Source§impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: TryFrom<T>,
impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: TryFrom<T>,
Source§exec fn obeys_try_from_spec() -> bool
exec fn obeys_try_from_spec() -> bool
Source§impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: TryInto<T>,
impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: TryInto<T>,
Source§exec fn obeys_try_into_spec() -> bool
exec fn obeys_try_into_spec() -> bool
Source§impl<T, U> TryIntoSpecImpl<U> for Twhere
U: TryFrom<T>,
impl<T, U> TryIntoSpecImpl<U> for Twhere
U: TryFrom<T>,
Source§open spec fn obeys_try_into_spec() -> bool
open spec fn obeys_try_into_spec() -> bool
{ <U as TryFromSpec<Self>>::obeys_try_from_spec() }