Expand description
Additional specifications for mutable BTreeMap operations not covered by vstd.
Structs§
- Cursor
MutModel - The abstract state of a mutable B-tree cursor.
- ExCursor
Mut - Verus declaration for Rust’s mutable B-tree cursor type.
Traits§
- Cursor
MutAdditional Spec Fns - Additional abstract and prophetic state for mutable B-tree cursors.
Functions§
- _verus_
external_ ⚠fn_ specification_ 0_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 1_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ lower__ bound__ mut_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 2_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ upper__ bound__ mut_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 3_ Cursor Mut_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ peek__ prev - _verus_
external_ ⚠fn_ specification_ 4_ Cursor Mut_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ peek__ next - axiom_
deref_ key_ cmp - axiom_
deref_ key_ ordering_ matches - axiom_
has_ resolved_ cursor - before_
lower_ bound - before_
upper_ bound - borrowed_
key_ cmp - borrowed_
key_ mutated - borrowed_
key_ ordering_ matches - group_
btree_ extra_ axioms - lemma_
borrowed_ key_ mutated_ deref - positioned_
at_ lower_ bound - positioned_
at_ upper_ bound