{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Agda.Builtin.String where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text

-- Agda.Builtin.String.String
type T_String_6 = Data.Text.Text
d_String_6 :: a
d_String_6
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.String.String"
-- Agda.Builtin.String.primStringUncons
d_primStringUncons_10 :: Text -> Maybe (Char, Text)
d_primStringUncons_10 = Text -> Maybe (Char, Text)
Data.Text.uncons
-- Agda.Builtin.String.primStringToList
d_primStringToList_12 :: Text -> [Char]
d_primStringToList_12 = Text -> [Char]
Data.Text.unpack
-- Agda.Builtin.String.primStringFromList
d_primStringFromList_14 :: [Char] -> Text
d_primStringFromList_14 = [Char] -> Text
Data.Text.pack
-- Agda.Builtin.String.primStringAppend
d_primStringAppend_16 :: Text -> Text -> Text
d_primStringAppend_16
  = ((Text -> Text -> Text
Data.Text.append) :: Data.Text.Text->Data.Text.Text->Data.Text.Text)
-- Agda.Builtin.String.primStringEquality
d_primStringEquality_18 :: Text -> Text -> Bool
d_primStringEquality_18
  = (\ Text
x Text
y -> (Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Data.Text.Text -> Data.Text.Text -> Bool) ( Text
x) ( Text
y))
-- Agda.Builtin.String.primShowChar
d_primShowChar_20 :: Char -> Text
d_primShowChar_20
  = ([Char] -> Text
Data.Text.pack ([Char] -> Text) -> (Char -> [Char]) -> Char -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> [Char]
forall a. Show a => a -> [Char]
show :: Char -> Data.Text.Text)
-- Agda.Builtin.String.primShowString
d_primShowString_22 :: Text -> Text
d_primShowString_22
  = ([Char] -> Text
Data.Text.pack ([Char] -> Text) -> (Text -> [Char]) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
forall a. Show a => a -> [Char]
show :: Data.Text.Text -> Data.Text.Text)
-- Agda.Builtin.String.primShowNat
d_primShowNat_24 :: Integer -> Text
d_primShowNat_24
  = ([Char] -> Text
Data.Text.pack ([Char] -> Text) -> (Integer -> [Char]) -> Integer -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> [Char]
forall a. Show a => a -> [Char]
show :: Integer -> Data.Text.Text)