def decide.sized.limits

mylsm-lsm-store@0.6.0.1 · src/scan/ByteBlockBuilder.bend:28

import Base

28def decide.sized.limits(
29  +used_bytes: Nat,
30  +record_bytes: Nat,
31  limits: Nat & Nat,
32  record_fits: Bool
33) -> Decision:
34  match limits:
35    case (current_cap, comparison_cap):
36      match record_fits:
37        case False{}: RecordTooLarge{}
38        case True{}:
39          decide.current(used_bytes, record_bytes,
40            Nat.is_le(Nat.add(used_bytes, record_bytes), comparison_cap))