vstd::modes

Function tracked_static_ref

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

Make any tracked object permanently shared and get a reference to it.

Tip: If you try to use this and run into problems relating to the introduction of a lifetime variable, you want to try Shared instead.