def del_hit_core

mylsm-lsm-store@0.6.0.1 · src/MemTable.bend:239

import Base
import mylsm-lsm-store@0.6.0.1/src/Keys.bend as Keys

239# Lemma: hit-reading a freshly-deleted key answers a tombstone hit.
240def del_hit_core(
241  +entries: List<&2, Entry>,
242  +key: String,
243) -> {scan_hit(List.length(&2, Entry, Con{Entry{key, None{}}, entries}), key, (False{}, None{}), Con{Entry{key, None{}}, entries}) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}:
244  %Equal.sym(Bool, Keys.eq(key, key), True{}, Keys.str_eq_refl(key)) : {scan_hit(List.length(&2, Entry, entries), key, scan_hit_step(False{}, _, None{}, None{}),
245  entries) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}
246  %frozen_hit_lemma(List.length(&2, Entry, entries), key, Some{None{}}, entries) : {scan_hit(List.length(&2, Entry, entries), key, (True{}, Some{None{}}), entries) == _ : Maybe<&2, Maybe<&2, String>>}
247  {==}