~/jendhub

def registry.release.input.bytes

mylsm-lsm-store@0.6.0.1 · src/scan/Snapshot.bend:374

import mylsm-lsm-store@0.6.0.1/src/scan/Snapshot.bend as Snapshot
import Base

374# Separates byte arithmetic inputs so both admission checks retain their values.
375def registry.release.input.bytes(
376  count_copies: Nat & Nat,
377  count_original: Nat,
378  bytes_copies: Nat & Nat,
379  bytes_original: Nat,
380  release_copies: Nat & Nat
381) -> RegistryReleaseDecision:
382  match count_copies:
383    case (count_for_subtract, count_for_check):
384      match bytes_copies:
385        case (bytes_for_subtract, bytes_for_check):
386          match release_copies:
387            case (released_for_subtract, released_for_check):
388              registry.release.result(
389                (Nat.sub(count_for_subtract, 1n),
390                  Nat.sub(bytes_for_subtract, released_for_subtract)),
391                Registry{count_original, bytes_original},
392                (Nat.is_lt(0n, count_for_check),
393                  Nat.is_le(released_for_check, bytes_for_check)))

Uses (9)

Used by (1)