Enum Either 

pub enum Either<L, R> {
    Left(L),
    Right(R),
}

A type containing either a Left value L or a Right value R.

Variants

Left(L)

Contains the left value

Right(R)

Contains the right value

Implementations

impl<L, R> Either<L, R>

pub exec fn left(self) -> Option<L>

Converts to the left value, if any.

pub fn __VERUS_SPEC_left(self) -> Option<L>

pub exec fn right(self) -> Option<R>

Converts to the right value, if any.

pub fn __VERUS_SPEC_right(self) -> Option<R>

pub exec fn is_left(&self) -> bool

Returns true if the left value is present.

pub fn __VERUS_SPEC_is_left(&self) -> bool

pub exec fn is_right(&self) -> bool

Returns true if the right value is present.

pub fn __VERUS_SPEC_is_right(&self) -> bool

Trait Implementations

impl<L: Clone, R: Clone> Clone for Either<L, R>

fn clone(&self) -> Either<L, R>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<L: Copy, R: Copy> Copy for Either<L, R>

impl<L: Debug, R: Debug> Debug for Either<L, R>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<L: Eq, R: Eq> Eq for Either<L, R>

impl<L: NonNullPtr, R: NonNullPtr> NonNullPtr for Either<L, R>

exec fn into_raw(self) -> ret : (NonNull<Self::Target>, Tracked<Self::Permission>)

unsafe exec fn from_raw( ptr: NonNull<Self::Target>, Tracked(perm): Tracked<Self::Permission>, ) -> Self

open spec fn ptr_perm_match(ptr: *mut Self::Target, perm: Self::Permission) -> bool

{
    let tag = 1usize << Self::ALIGN_BITS;
    match perm {
        Sum::Left(left) => (
            &&& ptr.addr() & tag == 0
            &&& L::ptr_perm_match(ptr.cast(), left)

        ),
        Sum::Right(right) => {
            let untagged_ptr = ptr.with_addr((ptr.addr() & !tag));
            let right_nonnull = nonnull_from_ptr_mut_spec(untagged_ptr);
            &&& ptr.addr() & tag == tag
            &&& (ptr.addr() & !tag) != 0
            &&& R::ptr_perm_match(right_nonnull.cast().view_ptr_mut(), right)

        }
    }
}

open spec fn rel_perm(self, perm: Self::Permission) -> bool

{
    match (self, perm) {
        (Either::Left(left), Sum::Left(left_perm)) => left.rel_perm(left_perm),
        (Either::Right(right), Sum::Right(right_perm)) => right.rel_perm(right_perm),
        _ => false,
    }
}

proof fn lemma_align_bits_range()

ensures

Self::ALIGN_BITS
    == if L::ALIGN_BITS < R::ALIGN_BITS { L::ALIGN_BITS - 1 } else { R::ALIGN_BITS - 1 },

const ALIGN_BITS: u32

The power of two of the pointer alignment.

type Target = PhantomData<Either<L, R>>

The target type that this pointer refers to.

type Permission = Sum<<L as NonNullPtr>::Permission, <R as NonNullPtr>::Permission>

A verification-only permission type that represents the ownership of the memory managed by the pointer.

impl<'a, L: NonNullPtrRef<'a>, R: NonNullPtrRef<'a>> NonNullPtrRef<'a> for Either<L, R>

open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission

{
    match perm {
        Sum::Left(left) => Sum::Left(L::ref_perm_view_permission(left)),
        Sum::Right(right) => Sum::Right(R::ref_perm_view_permission(right)),
    }
}

open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool

{ true }

proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission)

proof fn borrow_ref_perm(tracked perm: &Self::RefPermission) -> tracked ret : Self::RefPermission

proof fn borrow_perm_as_ref_perm(tracked perm: &'a Self::Permission) -> tracked ret : Self::RefPermission

unsafe exec fn raw_as_ref( raw: NonNull<Self::Target>, Tracked(perm): Tracked<Self::RefPermission>, ) -> Self::Ref

exec fn ref_as_raw( ptr_ref: Self::Ref, ) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>)

type Ref = Either<<L as NonNullPtrRef<'a>>::Ref, <R as NonNullPtrRef<'a>>::Ref>

type RefPermission = Sum<<L as NonNullPtrRef<'a>>::RefPermission, <R as NonNullPtrRef<'a>>::RefPermission>

A verification-only permission type that represents the reading permission of the memory managed by the pointer.

impl<L: PartialEq, R: PartialEq> PartialEq for Either<L, R>

fn eq(&self, other: &Either<L, R>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<L: PartialEq, R: PartialEq> StructuralPartialEq for Either<L, R>