Trait CursorMutAdditionalSpecFns 

pub trait CursorMutAdditionalSpecFns<Key, Value>: Sized {
    // Required methods
    spec fn view(&self) -> CursorMutModel<Key, Value>;
    spec fn final_map(self) -> Map<Key, Value>;
}

Additional abstract and prophetic state for mutable B-tree cursors.

Required Methods

spec fn view(&self) -> CursorMutModel<Key, Value>

spec fn final_map(self) -> Map<Key, Value>

The contents of the borrowed map when this cursor’s borrow is resolved.

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<'a, Key, Value, A> CursorMutAdditionalSpecFns<Key, Value> for CursorMut<'a, Key, Value, A>

uninterp spec fn view(&self) -> CursorMutModel<Key, Value>

uninterp spec fn final_map(self) -> Map<Key, Value>

Implementors