def frozen_lemma

mylsm-lsm-store@0.3.2.0 · src/MemTable.bend:97

import Base

97# Lemma: a frozen (done) scan always answers ans.
98def frozen_lemma(fuel: Nat, key: String, ans: Maybe<&2, String>, entries: List<&2, Entry>) -> {scan_go(fuel, key, (True{}, ans), entries) == ans : Maybe<&2, String>}:
99  match fuel:
100    case 0n:
101      {==}
102    case 1n+f:
103      match entries:
104        case Nil{}:
105          {==}
106        case Con{Entry{ekey, val}, t}:
107          %frozen_lemma(f, key, ans, t) : {scan_go(f, key, (True{}, ans), t) == _ : Maybe<&2, String>}
108          {==}