Struct CursorMutModel 

pub struct CursorMutModel<Key, Value> {
    pub keys: Seq<Key>,
    pub position: int,
    pub map: Map<Key, Value>,
}

The abstract state of a mutable B-tree cursor.

A cursor points at the gap immediately before keys[position]. Therefore peek_next accesses keys[position], while peek_prev accesses keys[position - 1].

Fields

keys: Seq<Key>

All keys in the underlying map, in strictly increasing order.

position: int

The index of the element immediately after the cursor.

map: Map<Key, Value>

The current contents of the complete map borrowed by the cursor.

Implementations

impl<Key, Value> CursorMutModel<Key, Value>

pub open spec fn wf(self) -> bool

{
    &&& 0 <= self.position <= self.keys.len()
    &&& self.keys.no_duplicates()
    &&& self.keys.to_set() == self.map.dom()
    &&& increasing_seq(self.keys)

}

Whether this model consistently represents an ordered map and a gap in that map.