MemTable.del_hit_core: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/MemTable.bend as MemTable
Lines 239-247 of mylsm-lsm-store@0.6.0.1/src/MemTable.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/MemTable.bend&start_line=239&end_line=247

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

# Lemma: hit-reading a freshly-deleted key answers a tombstone hit.
def del_hit_core(
  +entries: List<&2, Entry>,
  +key: String,
) -> {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>>}:
  %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{}),
  entries) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}
  %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>>}
  {==}

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/Keys.bend&name=eq
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/Keys.bend&name=str_eq_refl
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/MemTable.bend&name=Entry
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/MemTable.bend&name=frozen_hit_lemma
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/MemTable.bend&name=scan_hit
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/MemTable.bend&name=scan_hit_step