arc_deref_spec

vstd_extra::external::deref

Function arc_deref_spec 

Source 
pub broadcast proof fn arc_deref_spec<T>(a: Arc<T>)
Expand description
ensures
#[trigger] *(a.deref_spec()) == *a,