pub open spec fn fresh_cursor_id<'rcu>(m: Map<CursorId, CursorEntry<'rcu>>) -> CursorIdExpand description
{ choose |id: CursorId| !m.dom().contains(id) }Picks a cursor id not currently in m.dom(). As above.
pub open spec fn fresh_cursor_id<'rcu>(m: Map<CursorId, CursorEntry<'rcu>>) -> CursorId{ choose |id: CursorId| !m.dom().contains(id) }Picks a cursor id not currently in m.dom(). As above.