def Valid

bendtorch-core@0.1.0.0 · src/storage/api.bend:308

import Base

308def Valid(+n: Nat, +history: List<&2, Effect>) -> Type:
309  match history:
310    case Nil{}:
311      Unit
312    case +effect <> +past:
313      match effect:
314        case Wrote{+i, w}:
315          {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool} & Valid(n, past)
316        case Kept{i}:
317          Valid(n, past)
318        case Left{}:
319          Valid(n, past)
320        case Right{}:
321          Valid(n, past)