IdrisDoc: Data.String.Extra

# Data.String.Extra

(+>) : String -> Char -> String

  Alias of `strSnoc`

      "AB" +> 'C'

  Fixity
    Left associative, precedence 5
(<+) : Char -> String -> String

  Alias of `strCons`

      'A' <+ "AB"

  Fixity
    Left associative, precedence 5
drop : (n : Nat) -> (input : String) -> String

  Remove the first `n` characters from a string. Returns the empty string if
  the input string is too short.

dropLast : (n : Nat) -> (input : String) -> String

  Remove the last `n` characters from a string. Returns the empty string if
  the input string is too short.

indent : (n : Nat) -> String -> String

  Indent a given string by `n` spaces.

indentLines : (n : Nat) -> String -> String

  Indent each line of a given string by `n` spaces.

index : (n : Nat) -> (input : String) -> Maybe Char

  Get a character from a string if the string is long enough.

join : (sep : String) -> Foldable t => (xs : t String) -> String

  Concatenate the strings from a `Foldable` containing strings, separated by
  the given string.

replicate : (n : Nat) -> (c : Char) -> String

  Produce a string by repeating the character `c` `n` times.

shrink : (n : Nat) -> (input : String) -> String

  Remove the first and last `n` characters from a string. Returns the empty
  string if the input string is too short.

strSnoc : String -> Char -> String

  Adds a character to the end of the specified string.

      strSnoc "AB" 'C'

      strSnoc "" 'A'

take : (n : Nat) -> (input : String) -> String

  Take the first `n` characters from a string. Returns the whole string
  if it's too short.

takeLast : (n : Nat) -> (input : String) -> String

  Take the last `n` characters from a string. Returns the whole string
  if it's too short.