{-# 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
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"
d_primStringUncons_10 :: Text -> Maybe (Char, Text)
d_primStringUncons_10 = Text -> Maybe (Char, Text)
Data.Text.uncons
d_primStringToList_12 :: Text -> [Char]
d_primStringToList_12 = Text -> [Char]
Data.Text.unpack
d_primStringFromList_14 :: [Char] -> Text
d_primStringFromList_14 = [Char] -> Text
Data.Text.pack
d_primStringAppend_16 :: Text -> Text -> Text
d_primStringAppend_16
= ((Text -> Text -> Text
Data.Text.append) :: Data.Text.Text->Data.Text.Text->Data.Text.Text)
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))
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)
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)
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)