Function vstd::std_specs::clone::ex_tracked_clone

pub exec fn ex_tracked_clone<T: Copy>(b: &Tracked<T>) -> res : Tracked<T>

Expand description

ensures

res == b,

Function vstd::std_specs::clone::ex_tracked_cloneCopy item path