pub uninterp fn obeys_key_model<Key: ?Sized>() -> bool
Expand description
Specifies whether a type Key
conforms to our requirements to be
a key in our hash table (and hash set) model.
The three requirements are (1) the hash function is deterministic,
(2) any two keys of type Key
are identical if and only if they
are considered equal by the executable ==
operator, and (3) the
executable Key::clone
function produces a result identical to
its input. Requirement (1) isn’t satisfied by having Key
implement Hash
, since this trait doesn’t mandate determinism.
The standard library has axioms that all primitive types and Box
es
thereof obey this model. If you want to use some other key
type MyKey
, you need to explicitly state your assumption that it
does so with
assume(vstd::std_specs::hash::obeys_key_model::<MyKey>())
.
In the future, we plan to devise a way for you to prove that it
does so, so that you don’t have to make such an assumption.