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),