def del_core

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

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

180# Lemma: reading a freshly-deleted key answers None (tombstone freezes).
181def del_core(
182  +entries: List<&2, Entry>,
183  +key: String,
184) -> {scan_go(List.length(&2, Entry, Con{Entry{key, None{}}, entries}), key, (False{}, None{}), Con{Entry{key, None{}}, entries}) == None{} : Maybe<&2, String>}:
185  %Equal.sym(Bool, Keys.eq(key, key), True{}, Keys.str_eq_refl(key)) : {scan_go(List.length(&2, Entry, entries), key, scan_step(False{}, _, None{}, None{}), entries) == None{} : Maybe<&2, String>}
186  %frozen_lemma(List.length(&2, Entry, entries), key, None{}, entries) : {scan_go(List.length(&2, Entry, entries), key, (True{}, None{}), entries) == _ : Maybe<&2, String>}
187  {==}