IdrisDoc: Prelude.Strings

# Prelude.Strings

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   ")

words : String -> List String

  Splits a string into a list of whitespace separated strings.

      words " A B C  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']]

unwords : List String -> String

  Joins the strings by spaces into a single string.

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

unpack : String -> List Char

  Turns a string into a list of characters.

      unpack "ABC"

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']]

unlines : List String -> String

  Joins the strings by newlines into a single string.

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

trim : String -> String

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

      trim " A\nB C "

toUpper : String -> String

  Uppercases all characters in the string.

      toLower "aBc12!"

toLower : String -> String

  Lowercases all characters in the string.

      toLower "aBc12!"

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

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

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

strTail : String -> String

  Returns the characters specified after the head of the string.

  Doesn't work for empty strings.

      strTail "AB"

      strTail "A"

strM : (x : String) -> StrM x
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

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

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

strHead : String -> Char

  Returns the first character in the specified string.

  Doesn't work for empty strings.

      strHead "A"

strCons : Char -> String -> String

  Adds a character to the front of the specified string.

      strCons 'A' "B"

      strCons 'A' ""

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

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

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

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"

singleton : Char -> String

  Creates a string of a single character.

      singleton 'A'

reverse : String -> String

  Reverses the elements within a String.

      reverse "ABC"

      reverse ""

pack : Foldable t => t Char -> String

  Turns a Foldable of characters into a string.

nullStr : String -> IO Bool

  Check if a supposed string was actually a null pointer

nullPtr : Ptr -> IO Bool

  Check if a foreign pointer is null

null : Ptr
ltrim : String -> String

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

      ltrim " A\nB"

      ltrim " \nAB"

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")

lines : String -> List String

  Splits a string into a list of newline separated strings.

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

length : String -> Nat

  Returns the length of the string.

      length ""

      length "ABC"

isSuffixOf : String -> String -> Bool
isPrefixOf : String -> String -> Bool
isInfixOf : String -> String -> Bool
foldr1 : (a -> a -> a) -> List a -> a
foldl1 : (a -> a -> a) -> List a -> a
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"

data StrM : String -> Type
  StrNil : StrM ""
  StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
(++) : String -> String -> String

  Appends two strings together.

      "AB" ++ "C"

  Fixity
    Left associative, precedence 7