------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive Bytestrings: IO operations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible #-}
module Data.Bytestring.IO.Primitive where
open import Agda.Builtin.String using (String)
open import Agda.Builtin.Unit using (⊤)
open import Data.Bytestring.Primitive using (Bytestring)
open import IO.Primitive.Core using (IO)
postulate
readFile : String → IO Bytestring
writeFile : String → Bytestring → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# FOREIGN GHC import Data.ByteString #-}
{-# COMPILE GHC readFile = Data.ByteString.readFile . T.unpack #-}
{-# COMPILE GHC writeFile = Data.ByteString.writeFile . T.unpack #-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4