Function vstd::modes::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.