Idris2Doc : Data.String

Data.String

AsList : String -> Type
A view of a string as a lazy linked list of characters
Totality: total
Constructors:
Nil : AsList ""
(::) : (c : Char) -> Lazy (AsListstr) -> AsList (strConscstr)
StrM : String -> Type
A view checking whether a string is empty
and, if not, returning its head and tail
Totality: total
Constructors:
StrNil : StrM ""
StrCons : (x : Char) -> (xs : String) -> StrM (strConsxxs)
asList : (str : String) -> AsListstr
To each string we can associate the lazy linked list of characters
it corresponds to once unpacked.
Totality: total
break : (Char -> Bool) -> String -> (String, String)
Splits the string into a part before the predicate
returns True and the rest of the string.

```idris example
break (== 'C') "ABCD"
```
```idris example
break (== 'C') "EFGH"
```
Totality: total
fastAppend : List String -> String
Totality: total
fastUnlines : List String -> String
Totality: total
isInfixOf : String -> String -> Bool
Totality: total
isPrefixOf : String -> String -> Bool
Totality: total
isSuffixOf : String -> String -> Bool
Totality: total
lines : String -> List1 String
Splits a string into a list of newline separated strings.

```idris example
lines "\rA BC\nD\r\nE\n"
```
Totality: total
lines' : List Char -> List1 (List Char)
Splits a character list into a list of newline separated character lists.

```idris example
lines' (unpack "\rA BC\nD\r\nE\n")
```
Totality: total
ltrim : String -> String
Trim whitespace on the left of the string
Totality: total
parseDouble : String -> Maybe Double
Convert a number string to a Double.

```idris example
parseDouble "+123.123e-2"
```
```idris example
parseDouble {a=Int} " -123.123E+2"
```
```idris example
parseDouble {a=Int} " +123.123"
```
parseInteger : (Numa, Nega) => String -> Maybea
Convert a number string to a Num.

```idris example
parseInteger " 123"
```
```idris example
parseInteger {a=Int} " -123"
```
Totality: total
parsePositive : Numa => String -> Maybea
Convert a positive number string to a Num.

```idris example
parsePositive "123"
```
```idris example
parsePositive {a=Int} " +123"
```
Totality: total
singleton : Char -> String
Totality: total
span : (Char -> Bool) -> String -> (String, String)
Splits the string into a part before the predicate
returns False and the rest of the string.

```idris example
span (/= 'C') "ABCD"
```
```idris example
span (/= 'C') "EFGH"
```
Totality: total
split : (Char -> Bool) -> String -> List1 String
Splits the string into parts with the predicate
indicating separator characters.

```idris example
split (== '.') ".AB.C..D"
```
Totality: total
strIndex : String -> Int -> Char
strLength : String -> Int
strM : (x : String) -> StrMx
To each string we can associate its StrM view
Totality: total
strSubstr : Int -> Int -> String -> String
strTail : String -> String
stringToNatOrZ : String -> Nat
Totality: total
toLower : String -> String
Totality: total
toUpper : String -> String
Totality: total
trim : String -> String
Trim whitespace on both sides of the string
Totality: total
unlines : List String -> String
Joins the strings by newlines into a single string.

```idris example
unlines ["line", "line2", "ln3", "D"]
```
Totality: total
unlines' : List (List Char) -> List Char
Joins the character lists by newlines into a single character list.

```idris example
unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]
```
Totality: total
unwords : List String -> String
Joins the strings by spaces into a single string.

```idris example
unwords ["A", "BC", "D", "E"]
```
Totality: total
words : String -> List String
Splits a string into a list of whitespace separated strings.

```idris example
words " A B C D E "
```