Function vstd::std_specs::clone::ex_ghost_clone

pub exec fn ex_ghost_clone<T>(b: &Ghost<T>) -> res : Ghost<T>

Expand description

ensures

res == b,

Function vstd::std_specs::clone::ex_ghost_cloneCopy item path