Trait SlicePointerExt 

pub trait SlicePointerExt<T>: PointerExt<[T]> {
    // Required methods
    fn thin(self) -> *const T;
    fn len_logic(self) -> usize;
    fn slice_ptr_ext(self, other: Self);
}

Extension methods for *const [T]

thin and len_logic are wrappers around _ as *const T and metadata_logic that also pull in the slice_ptr_ext axiom when used.

Required Methods

fn thin(self) -> *const T

Remove metadata.

logic

fn len_logic(self) -> usize

Get the metadata.

logic

fn slice_ptr_ext(self, other: Self)

Extensionality law.

logic(law)

ensures

self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<T> SlicePointerExt<T> for *const [T]

fn thin(self) -> *const T

Convert *const [T] to *const T.

logic(open, inline)

self as *const T

fn len_logic(self) -> usize

Get the length metadata of the pointer.

logic(open, inline)

metadata_logic(self)

fn slice_ptr_ext(self, other: Self)

Extensionality of slice pointers.

logic(law)

ensures

self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other

impl<T> SlicePointerExt<T> for *mut [T]

fn thin(self) -> *const T

Convert *const [T] to *const T.

logic(open, inline)

self as *const T

fn len_logic(self) -> usize

Get the length metadata of the pointer.

logic(open, inline)

metadata_logic(self as *const [T])

fn slice_ptr_ext(self, other: Self)

Extensionality of slice pointers.

logic(law)

ensures

self.thin() == other.thin() && self.len_logic() == other.len_logic() ==> self == other

Implementors