ByteSstFile.page.next.cloned: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/ByteSstFile.bend as ByteSstFile
Lines 405-416 of mylsm-lsm-store@0.6.0.1/src/ByteSstFile.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/ByteSstFile.bend&start_line=405&end_line=416

import Base
import mylsm-lsm-store@0.6.0.1/src/ByteMemTable.bend as ByteMemTable
import mylsm-lsm-store@0.6.0.1/src/StorageBytes.bend as StorageBytes
import mylsm-lsm-store@0.6.0.1/src/scan/ByteBlockBuilder.bend as ByteBlockBuilder

def page.next.cloned(
  tail: List<&1, ByteMemTable.Entry>,
  current_count: Nat,
  current_bytes: Nat,
  +max_bytes: Nat,
  copies: ByteMemTable.Entry & ByteMemTable.Entry
) -> List<&1, ByteMemTable.Entry> & ByteBlockBuilder.Decision:
  match copies:
    case (for_decision, for_remaining):
      (Con{for_remaining, tail}, ByteBlockBuilder.decide.target(current_bytes,
        page.record.required(for_decision, Nat.is_gt(current_count, 0n)),
        Nat.min(U32.to_nat(StorageBytes.TARGET_BLOCK_BYTES()), max_bytes), max_bytes))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_gt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.min
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/ByteMemTable.bend&name=Entry
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/ByteSstFile.bend&name=page.record.required
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/StorageBytes.bend&name=TARGET_BLOCK_BYTES
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/ByteBlockBuilder.bend&name=Decision
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/scan/ByteBlockBuilder.bend&name=decide.target