BackupCursor.finish.copied: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/transfer/BackupCursor.bend as BackupCursor
Lines 264-280 of mylsm-lsm-store@0.6.0.1/src/transfer/BackupCursor.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/BackupCursor.bend&start_line=264&end_line=280

import Base
import mylsm-lsm-store@0.6.0.1/src/ByteMemTable.bend as ByteMemTable
import mylsm-lsm-store@0.6.0.1/src/scan/VisibleCursor.bend as VisibleCursor
import mylsm-lsm-store@0.6.0.1/src/transfer/BackupCursorPolicy.bend as Policy

def finish.copied(
  cursor: Maybe<&1, VisibleCursor.Cursor>,
  pending: List<&1, ByteMemTable.Entry>,
  pending_count: Nat,
  seen_copies: Nat & Nat,
  expected_copies: Nat & Nat,
  entry_count: U32,
  block_count: U32,
  block_index: U32
) -> Step:
  match seen_copies:
    case (seen_check, seen_retained):
      match expected_copies:
        case (expected_check, expected_retained):
          finish.decided(Policy.finish(seen_check, expected_check, pending_count),
            cursor, pending, seen_retained, expected_retained, entry_count,
            block_count, block_index)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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
  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/scan/VisibleCursor.bend&name=Cursor
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/BackupCursor.bend&name=Step
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/BackupCursor.bend&name=finish.decided
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/BackupCursorPolicy.bend&name=finish