Idris2Doc : Data.String

Data.String

dataAsList : 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)
dataStrM : 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 : ListString -> String
Totality: total
fastUnlines : ListString -> String
Totality: total
indent : Nat -> String -> String
  Indent a given string by `n` spaces.

Totality: total
isInfixOf : String -> String -> Bool
Totality: total
isPrefixOf : String -> String -> Bool
Totality: total
isSuffixOf : String -> String -> Bool
Totality: total
lines : String -> ListString
  Splits a string into a list of newline separated strings.

```idris example
lines "\rA BC\nD\r\nE\n"
```

Totality: total
lines' : ListChar -> List (ListChar)
  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
null : String -> Bool
Totality: total
padLeft : Nat -> Char -> String -> String
  Pad a string on the left

Totality: total
padRight : Nat -> Char -> String -> String
  Pad a string on the right

Totality: total
parseDouble : String -> MaybeDouble
  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
replicate : Nat -> Char -> String
  Create a string by using n copies of a character

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 -> List1String
  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 : ListString -> String
  Joins the strings into a single string by appending a newline to each string.

```idris example
unlines ["line", "line2", "ln3", "D"]
```

Totality: total
unlines' : List (ListChar) -> ListChar
  Joins the character lists by a single character list by appending a newline
to each line.

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

Totality: total
unwords : ListString -> String
  Joins the strings by spaces into a single string.

```idris example
unwords ["A", "BC", "D", "E"]
```

Totality: total
words : String -> ListString
  Splits a string into a list of whitespace separated strings.

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