MemTable.ryw_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 217-227 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=217&end_line=227

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

# Lemma: hit-reading a freshly-put key answers a value hit.
def ryw_hit_core(
  +entries: List<&2, Entry>,
  +key: String,
  val: String,
) -> {scan_hit(List.length(&2, Entry, Con{Entry{key, Some{val}}, entries}), key, (False{}, None{}), Con{Entry{key, Some{val}}, entries}) == Some{Some{val}} : 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{}, _, Some{val}, None{}),
  entries) == Some{Some{val}} : Maybe<&2, Maybe<&2, String>>}
  %frozen_hit_lemma(List.length(&2, Entry, entries), key, Some{Some{val}}, entries) : {scan_hit(List.length(&2, Entry, entries), key, (True{}, Some{Some{val}}),
  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