Skip to main content

tracked_static_mut_ref

vstd::modes

Function tracked_static_mut_ref 

Source 
pub proof fn tracked_static_mut_ref<V>(tracked v: V) -> tracked res : &'static mut V
Expand description
ensures
*res == v,

Make any tracked object permanently mutably borrowed.