def frozen_hit_lemma

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

import Base

199# Lemma: a frozen hit-scan always answers ans.
200def frozen_hit_lemma(
201  fuel: Nat,
202  key: String,
203  ans: Maybe<&2, Maybe<&2, String>>,
204  entries: List<&2, Entry>
205) -> {scan_hit(fuel, key, (True{}, ans), entries) == ans : Maybe<&2, Maybe<&2, String>>}:
206  match fuel:
207    case 0n:
208      {==}
209    case 1n+f:
210      match entries:
211        case Nil{}:
212          {==}
213        case Con{Entry{ekey, val}, t}:
214          %frozen_hit_lemma(f, key, ans, t) : {scan_hit(f, key, (True{}, ans), t) == _ : Maybe<&2, Maybe<&2, String>>}
215          {==}