------------------------------------------------------------------------
-- The Agda standard library
--
-- Bytestrings: IO operations
------------------------------------------------------------------------

{-# OPTIONS --guardedness --cubical-compatible #-}

module Data.Bytestring.IO where

open import Agda.Builtin.String using (String)
open import IO using (IO; lift)
open import Data.Bytestring.Base using (Bytestring)
open import Data.Unit.Base using (⊤)

import Data.Bytestring.IO.Primitive as Prim

readFile : String → IO Bytestring
readFile fp = lift (Prim.readFile fp)

writeFile : String → Bytestring → IO ⊤
writeFile fp str = lift (Prim.writeFile fp str)