rc_deref_spec
vstd_
extra
In vstd_
extra::
external::
deref
vstd_extra
::
external
::
deref
Function
rc_
deref_
spec
Copy item path
Source
pub
broadcast proof
fn rc_deref_spec<T>(r:
Rc
<T>)
Expand description
ensures
#[trigger]
*
(r.deref_spec()) ==
*
r,