BackupIo.destination.checked: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/transfer/BackupIo.bend as BackupIo
Lines 236-250 of mylsm-lsm-store@0.6.0.1/src/transfer/BackupIo.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/BackupIo.bend&start_line=236&end_line=250

import Base
import mylsm-lsm-store@0.6.0.1/src/transfer/Backup.bend as Backup
import mylsm-lsm-store@0.6.0.1/src/Fs.bend as Fs

def destination.checked(
  +destination: String,
  +temporary: String,
  exists: Result<&1, &1, U32 & String, Bool>,
  stream: Backup.Stream,
  fuel: Nat
) -> IO(Result<&1, &1, Error, Unit>):
  match exists:
    case Fail{(code, message)}:
      IO.pure(Result<&1, &1, Error, Unit>, Fail{Io{code, message}})
    case Done{True{}}: IO.pure(Result<&1, &1, Error, Unit>, Fail{AlreadyExists{}})
    case Done{False{}}:
      do IO<Result<&1, &1, Error, Unit>>:
        created : Result<&1, &1, U32 & String, Unit> <- Fs.make_dir(path.clone(temporary))
        directory.created(destination, temporary, created, stream, fuel)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.bind
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.pure
  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=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/Fs.bend&name=make_dir
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/Backup.bend&name=Stream
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/BackupIo.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/BackupIo.bend&name=directory.created
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/BackupIo.bend&name=path.clone