def frozen_lemma

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

import Base

141# Lemma: a frozen (done) scan always answers ans.
142def frozen_lemma(
143  fuel: Nat,
144  key: String,
145  ans: Maybe<&2, String>,
146  entries: List<&2, Entry>
147) -> {scan_go(fuel, key, (True{}, ans), entries) == ans : Maybe<&2, String>}:
148  match fuel:
149    case 0n:
150      {==}
151    case 1n+f:
152      match entries:
153        case Nil{}:
154          {==}
155        case Con{Entry{ekey, val}, t}:
156          %frozen_lemma(f, key, ans, t) : {scan_go(f, key, (True{}, ans), t) == _ : Maybe<&2, String>}
157          {==}