structure Network.Wai.Middleware.Push.Referer.LRU (α β : Type) [BEq α] : Type

A simple LRU cache mapping keys to values. Items are ordered most-recently-used first.

• maxSize : Nat

  Maximum cache size.

• entries : List (α × β)

  Entries ordered by access time (most recent first).

@[implicit_reducible]

instance Network.Wai.Middleware.Push.Referer.instReprLRU {α✝ β✝ : Type} {inst✝ : BEq α✝} [Repr α✝] [Repr β✝] : Repr (LRU α✝ β✝)

Equations

• Network.Wai.Middleware.Push.Referer.instReprLRU = { reprPrec := Network.Wai.Middleware.Push.Referer.instReprLRU.repr }

def Network.Wai.Middleware.Push.Referer.instReprLRU.repr {α✝ β✝ : Type} {inst✝ : BEq α✝} [Repr α✝] [Repr β✝] : LRU α✝ β✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Network.Wai.Middleware.Push.Referer.LRU.empty {α β : Type} [BEq α] (maxSize : Nat) : LRU α β

Create an empty LRU cache.

Equations

• Network.Wai.Middleware.Push.Referer.LRU.empty maxSize = { maxSize := maxSize, entries := [] }

def Network.Wai.Middleware.Push.Referer.LRU.lookup {α β : Type} [BEq α] (key : α) (cache : LRU α β) : Option β × LRU α β

Look up a key, moving it to the front if found.

Equations

• One or more equations did not get rendered due to their size.

def Network.Wai.Middleware.Push.Referer.LRU.insert {α β : Type} [BEq α] (key : α) (val : β) (cache : LRU α β) : LRU α β

Insert a key-value pair, evicting the LRU entry if at capacity.

Equations

• One or more equations did not get rendered due to their size.

def Network.Wai.Middleware.Push.Referer.LRU.size {α β : Type} [BEq α] (cache : LRU α β) : Nat

Get the current size.

Equations

• cache.size = cache.entries.length