------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive Bytestrings: builder type and functions
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible #-}
module Data.Bytestring.Builder.Primitive where
open import Agda.Builtin.String using (String)
open import Data.Bytestring.Primitive using (Bytestring)
open import Data.Word8.Primitive using (Word8)
infixr 6 _<>_
postulate
-- Builder and execution
Builder : Set
toBytestring : Builder → Bytestring
-- Assembling a builder
bytestring : Bytestring → Builder
word8 : Word8 → Builder
empty : Builder
_<>_ : Builder → Builder → Builder
{-# FOREIGN GHC import qualified Data.ByteString.Builder as Builder #-}
{-# FOREIGN GHC import qualified Data.ByteString.Lazy as Lazy #-}
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC Builder = type Builder.Builder #-}
{-# COMPILE GHC toBytestring = Lazy.toStrict . Builder.toLazyByteString #-}
{-# COMPILE GHC bytestring = Builder.byteString #-}
{-# COMPILE GHC word8 = Builder.word8 #-}
{-# COMPILE GHC empty = mempty #-}
{-# COMPILE GHC _<>_ = mappend #-}
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