Function vstd::std_specs::clone::ex_ghost_clone

source · 
pub exec fn ex_ghost_clone<T>(b: &Ghost<T>) -> res : Ghost<T>
Expand description
ensures
res == b,