Trait NonNullExt 

pub trait NonNullExt {
    // Required method
    fn view_inj(n1: Self, n2: Self);
}

Additional lemmas for NonNull.

Required Methods

fn view_inj(n1: Self, n2: Self)

logic

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: ?Sized> NonNullExt for NonNull<T>

fn view_inj(n1: Self, n2: Self)

Asserts that the NonNull is only defined by the contained pointer.

logic

ensures

n1@ == n2@ ==> n1 == n2

Implementors