def add_room

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/src/cache.bend:123

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/types/model.bend as T

123def add_room(-K: Data, -V: Data, +c: Cache<K, V>, code: String, key: K, value: V, deadline: T.Int64, full: Bool) -> Step<K, V>:
124  match full:
125    case False{}:
126      store(K, V, c, code, key, value, deadline, False{}, Nil{})
127    case True{}:
128      store_after_evict(K, V, code, key, value, deadline, remove_oldest(K, V, c, True{}))