Skip to main content

fresh_list_id

ostd::specs::mm::embedding::list_store

Function fresh_list_id 

Source 
pub open spec fn fresh_list_id<M: AnyFrameMeta + Repr<MetaSlotSmall>>(
    lists: Map<ListId, LinkedListOwner<M>>,
    cursors: Map<CursorId, CursorOwner<M>>,
) -> ListId
Expand description
{ choose |id: ListId| !lists.dom().contains(id) && !cursors.dom().contains(id) }

Fresh-id helper for the list id space. The id must avoid both held lists and checked-out cursors (a cursored list’s home id is absent from lists but reserved in cursors).