Idris2Doc : Data.LRUCache1

Data.LRUCache1

(source)
Linear Least Recently Used (LRU) Cache

Reexports

importpublic Data.HashPSQ
importpublic Data.LRUCache.Internal
importpublic Data.LRUCache1.Internal

Definitions

empty : Nat->F1s (LRUCache1skv)
  Create an empty LRUCache1 of the given size.

Totality: total
Visibility: export
insert : Hashablek=>Ordk=>k->v->LRUCache1skv->F1s (LRUCache1skv)
  Insert an element into the LRUCache1.

Totality: total
Visibility: export
insertView : Hashablek=>Ordk=>k->v->LRUCache1skv->F1s (Maybe (k, v), LRUCache1skv)
  Insert an element into the LRUCache1 returning the evicted element if any.
When the logical clock reaches its maximum value and all values are
evicted Nothing is returned.

Totality: total
Visibility: export
lookup : Hashablek=>Ordk=>k->LRUCache1skv->F1s (Maybe (v, LRUCache1skv))
  Lookup an element in an LRUCache1 and mark it as the least recently accessed.

Totality: total
Visibility: export
toList : Hashablek=>Ordk=>LRUCache1skv->F1s (List (k, v))
  Convert an LRUCache1 to a list of (key, value) pairs.

Totality: total
Visibility: export