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 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() }