IdrisDoc: Effect.File.FileResult

# Effect.File.FileResult

FileOpResult : Type -> Type

  Type alias to describe a file operatons that returns a result.

data FileOpReturnTy : (desc : ResultDesc) -> (ty : Type) -> Type

  A custom return type for file operations that is dependent on
  the type of file operation.

  desc

    Parameterises the constructors to describe if the function
    returns a value or not.

  ty

    The return type for a file operation that returns a value.

  Success : FileOpReturnTy SUCCESS ty

    The operation completed successfully and doesn't return a
    result.

  Result : ty -> FileOpReturnTy RESULT ty

    The operation returns a result of type `ty`.

    ty

      The value returned.

  FError : (err : FileError) -> FileOpReturnTy desc ty

    The operation failed and the RTS produced the given error.

    err

      The reported error code.

FileOpSuccess : Type

  Type alias to describe file oeprations that indicate success.

data ResultDesc : Type

  A type to describe the return type of file operations.

  SUCCESS : ResultDesc
  RESULT : ResultDesc