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.

fn len_logic(self) -> usize

Get the metadata.

fn slice_ptr_ext(self, other: Self)

Extensionality law.

(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", so this trait is not object safe.

Implementations on Foreign Types

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

fn thin(self) -> *const T

Convert *const [T] to *const T.

(open, inline)

self as *const T

fn len_logic(self) -> usize

Get the length metadata of the pointer.

(open, inline)

pearlite! { metadata_logic(self) }

fn slice_ptr_ext(self, other: Self)

Extensionality of slice pointers.

(law)

ensures

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

Implementors