- data AsList : String -> Type
A view of a string as a lazy linked list of characters
Totality: total
Constructors:
- Nil : AsList ""
- (::) : (c : Char) -> Lazy (AsList str) -> AsList (strCons c str)
- data 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 (strCons x xs)
- asList : (str : String) -> AsList str
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
- 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 -> List 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 -> List (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- 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 -> 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 : (Num a, Neg a) => String -> Maybe a
Convert a number string to a Num.
```idris example
parseInteger " 123"
```
```idris example
parseInteger {a=Int} " -123"
```
Totality: total- parsePositive : Num a => String -> Maybe a
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 -> 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) -> StrM x
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 into a single string by appending a newline to each string.
```idris example
unlines ["line", "line2", "ln3", "D"]
```
Totality: total- unlines' : List (List Char) -> List Char
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 : 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 "
```