Function fresh_segment_id Copy item path

pub open spec fn fresh_segment_id(m: Map<SegmentId, SegmentEntry>) -> SegmentId

{ choose |id: SegmentId| !m.dom().contains(id) }