Prelude.Strings

(++) : String -> String -> String

Appends two strings together.

"AB" ++ "C"

Fixity

Left associative, precedence 7

data StrM : String -> Type

StrNil : StrM ""

StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)

data StringBuffer : Type

A preallocated buffer for building a String. This allows a function (in IO)
to allocate enough space for a string which will be built from smaller
pieces without having to allocate at every step.
To build a string using a StringBuffer, see newStringBuffer,
addToStringBuffer and getStringFromBuffer.

MkString : Ptr -> StringBuffer

addToStringBuffer : StringBuffer -> String -> IO ()

Append a string to the end of a string buffer

break : (Char -> Bool) -> String -> (String, String)

Splits the string into a part before the predicate
returns True and the rest of the string.

break (== 'C') "ABCD"

break (== 'C') "EFGH"

foldl1 : (a -> a -> a) -> List a -> a

foldr1 : (a -> a -> a) -> List a -> a

getStringFromBuffer : StringBuffer -> IO String

Get the string from a string buffer. The buffer is invalid after
this.

isInfixOf : String -> String -> Bool

isPrefixOf : String -> String -> Bool

isSuffixOf : String -> String -> Bool

length : String -> Nat

Returns the length of the string.

length ""

length "ABC"

lines : String -> List String

Splits a string into a list of newline separated strings.

lines  "\rA BC\nD\r\nE\n"

lines' : List Char -> List (List Char)

Splits a character list into a list of newline separated character lists.

lines' (unpack "\rA BC\nD\r\nE\n")

ltrim : String -> String

Removes whitespace (determined by 'isSpace') from
the start of the string.

ltrim " A\nB"

ltrim " \nAB"

managedNull : ManagedPtr

newStringBuffer : (len : Int) -> IO StringBuffer

Create a buffer for a string with maximum length len

null : Ptr

nullManagedPtr : ManagedPtr -> IO Bool

nullPtr : Ptr -> IO Bool

Check if a foreign pointer is null

nullStr : String -> IO Bool

Check if a supposed string was actually a null pointer

pack : Foldable t => t Char -> String

Turns a Foldable of characters into a string.

reverse : String -> String

Reverses the elements within a String.

reverse "ABC"

reverse ""

singleton : Char -> String

Creates a string of a single character.

singleton 'A'

span : (Char -> Bool) -> String -> (String, String)

Splits the string into a part before the predicate
returns False and the rest of the string.

span (/= 'C') "ABCD"

span (/= 'C') "EFGH"

split : (Char -> Bool) -> String -> List String

Splits the string into parts with the predicate
indicating separator characters.

split (== '.') ".AB.C..D"

strCons : Char -> String -> String

Adds a character to the front of the specified string.

strCons 'A' "B"

strCons 'A' ""

strHead : String -> Char

Returns the first character in the specified string.

Doesn't work for empty strings.

strHead "A"

strHead' : (x : String) -> (not (x == "") = True) -> Char

Version of 'strHead' that statically verifies that the string is not empty.

strIndex : String -> Int -> Char

Returns the nth character (starting from 0) of the specified string.

Precondition: '0 < i < length s' for 'strIndex s i'.

strIndex "AB" 1

strM : (x : String) -> StrM x

strTail : String -> String

Returns the characters specified after the head of the string.

Doesn't work for empty strings.

strTail "AB"

strTail "A"

strTail' : (x : String) -> (not (x == "") = True) -> String

Version of 'strTail' that statically verifies that the string is not empty.

substr : (index : Nat) -> (len : Nat) -> (subject : String) -> String

Returns a substring of a given string

index

The (zero based) index of the string to extract. If this is
beyond the end of the string, the function returns the empty
string.

len

The desired length of the substring. Truncated if this exceeds
the length of the input.

subject

The string to return a portion of

toLower : String -> String

Lowercases all characters in the string.

toLower "aBc12!"

toUpper : String -> String

Uppercases all characters in the string.

toUpper "aBc12!"

trim : String -> String

Removes whitespace (determined by 'isSpace') from
the start and end of the string.

trim " A\nB C "

unlines : List String -> String

Joins the strings by newlines into a single string.

unlines ["line", "line2", "ln3", "D"]

unlines' : List (List Char) -> List Char

Joins the character lists by newlines into a single character list.

unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]

unpack : String -> List Char

Turns a string into a list of characters.

unpack "ABC"

unwords : List String -> String

Joins the strings by spaces into a single string.

unwords ["A", "BC", "D", "E"]

unwords' : List (List Char) -> List Char

Joins the character lists by spaces into a single character list.

unwords' [['A'], ['B', 'C'], ['D'], ['E']]

words : String -> List String

Splits a string into a list of whitespace separated strings.

words " A B C  D E   "

words' : List Char -> List (List Char)

Splits a character list into a list of whitespace separated character lists.

words' (unpack " A B C  D E   ")