Function vstd::pervasive::cloned

source · 
pub open spec fn cloned<T: Clone>(a: T, b: T) -> bool
Expand description
{ strictly_cloned(a, b) || a == b }

Predicate indicating b is “a clone” of a; i.e., b could be the result of calling a.clone() or is equal to a.

By always considering a value to be a clone of itself, regardless of the definition of T::clone, this definition is useful in places where ‘clone’ calls might be optimized to copies. This is particularly common in the Rust stdlib.