Trait BorrowSpecImpl 

pub trait BorrowSpecImpl<Borrowed: ?Sized>: Borrow<Borrowed> {
    // Required methods
    exec fn obeys_borrow_spec() -> bool;
    exec fn borrow_spec(&self) -> &Borrowed;
}

Required Methods

exec fn obeys_borrow_spec() -> bool

exec fn borrow_spec(&self) -> &Borrowed

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl BorrowSpecImpl<str> for String

Available on crate feature alloc and non-verus_verify_core only.

open spec fn obeys_borrow_spec() -> bool

{ true }

uninterp spec fn borrow_spec(&self) -> &str

impl<T: ?Sized, A: Allocator> BorrowSpecImpl<T> for Box<T, A>

Available on crate feature alloc only.

open spec fn obeys_borrow_spec() -> bool

{ true }

open spec fn borrow_spec(&self) -> &T

{ &**self }

impl<T: ?Sized> BorrowSpecImpl<T> for &T

open spec fn obeys_borrow_spec() -> bool

{ true }

open spec fn borrow_spec(&self) -> &T

{ *self }

Implementors

impl<T: ?Sized> BorrowSpecImpl<T> for T