Function vstd::ptr::points_to_height_axiom
source · pub fn points_to_height_axiom<V>(points_to: PointsTo<V>)👎Deprecated: The vstd::ptr version of PPtr is deprecated. Use either:
–
PPtr<T> in vstd::simple_pptr (for simple use-cases, with fixed-size typed heap allocations)
– *mut T with vstd::raw_ptr (for more advanced use-cases)Expand description
ensures
#[trigger] is_smaller_than(points_to@, points_to),