Data.String

Reexports

Definitions

singleton : Char -> String

Totality: total
Visibility: public export

replicate : Nat -> Char -> String

  Create a string by using n copies of a character

Totality: total
Visibility: public export

indent : Nat -> String -> String

  Indent a given string by `n` spaces.

Totality: total
Visibility: public export

padLeft : Nat -> Char -> String -> String

  Pad a string on the left

Totality: total
Visibility: public export

padRight : Nat -> Char -> String -> String

  Pad a string on the right

Totality: total
Visibility: public export

fastUnlines : List String -> String

Totality: total
Visibility: export

words : String -> List String

  Splits a string into a list of whitespace separated strings.
  
  ```idris example
  words " A B C  D E   "
  ```

Totality: total
Visibility: public export

joinBy : String -> List String -> String

  Joins the strings using the provided separator
  ```idris example
  joinBy ", " ["A", "BC", "D"] === "A, BC, D"
  ```

Totality: total
Visibility: public export

unwords : List String -> String

  Joins the strings by spaces into a single string.
  
  ```idris example
  unwords ["A", "BC", "D", "E"] === "A BC D E"
  ```

Totality: total
Visibility: public export

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

  Splits a character list into a list of newline separated character lists.
  
  The empty string becomes an empty list. The last newline, if not followed by
  any additional characters, is eaten (there will never be an empty string last element
  in the result).
  
  ```idris example
  lines' (unpack "\rA BC\nD\r\nE\n")
  ```

Totality: total
Visibility: public export

lines : String -> List String

  Splits a string into a list of newline separated strings.
  
  The empty string becomes an empty list. The last newline, if not followed by
  any additional characters, is eaten (there will never be an empty string last element
  in the result).
  
  ```idris example
  lines  "\rA BC\nD\r\nE\n"
  ```

Totality: total
Visibility: public export

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
Visibility: public export

data StrM : String -> Type

  A view checking whether a string is empty
  and, if not, returning its head and tail

Totality: total
Visibility: public export
Constructors:

StrNil : StrM ""

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

strM : (x : String) -> StrM x

  To each string we can associate its StrM view

Totality: total
Visibility: public export

data AsList : String -> Type

  A view of a string as a lazy linked list of characters

Totality: total
Visibility: public export
Constructors:

Nil : AsList ""

(::) : (c : Char) -> Lazy (AsList str) -> AsList (strCons c str)

asList : (str : String) -> AsList str

  To each string we can associate the lazy linked list of characters
  it corresponds to once unpacked.

Totality: total
Visibility: public export

ltrim : String -> String

  Trim whitespace on the left of the string

Totality: total
Visibility: public export

trim : String -> String

  Trim whitespace on both sides of the string

Totality: total
Visibility: public export

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
Visibility: public export

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
Visibility: public export

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
Visibility: public export

stringToNatOrZ : String -> Nat

Totality: total
Visibility: public export

toUpper : String -> String

Totality: total
Visibility: public export

toLower : String -> String

Totality: total
Visibility: public export

strIndex : String -> Int -> Char

Visibility: public export

strLength : String -> Int

Visibility: public export

strSubstr : Int -> Int -> String -> String

Visibility: public export

strTail : String -> String

Visibility: public export

isPrefixOf : String -> String -> Bool

Totality: total
Visibility: public export

isSuffixOf : String -> String -> Bool

Totality: total
Visibility: public export

isInfixOf : String -> String -> Bool

Totality: total
Visibility: public export

parseNumWithoutSign : List Char -> Integer -> Maybe Integer

Totality: total
Visibility: public export

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
Visibility: public export

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
Visibility: public export

parseDouble : String -> Maybe Double

  Convert a number string to a Double.
  
  ```idris example
  parseDouble "+123.123e-2"
  ```
  ```idris example
  parseDouble " -123.123E+2"
  ```
  ```idris example
  parseDouble " +123.123"
  ```

Visibility: export

null : String -> Bool

Totality: total
Visibility: public export