vstd::pervasive

Function strictly_cloned

Source 
pub open spec fn strictly_cloned<T: Clone>(a: T, b: T) -> bool
Expand description
{ call_ensures(T::clone, (&a,), b) }

Predicate indicating b could be the result of calling a.clone()

It is usually recommended to use cloned instead, which takes the reflexive closure.