Data.String.Extra

Definitions

strSnoc : String -> Char -> String

  Adds a character to the end of the specified string.
  
  ```idris example
  strSnoc "AB" 'C'
  ```
  ```idris example
  strSnoc "" 'A'
  ```

Totality: total
Visibility: public export

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

  Alias of `strSnoc`
  
  ```idris example
  "AB" +> 'C'
  ```

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5

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

  Alias of `strCons`
  
  ```idris example
  'A' <+ "AB"
  ```

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 5

take : Nat -> String -> String

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

Totality: total
Visibility: public export

takeLast : Nat -> String -> String

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

Totality: total
Visibility: public export

drop : Nat -> String -> String

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

Totality: total
Visibility: public export

dropLast : Nat -> String -> String

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

Totality: total
Visibility: public export

shrink : Nat -> String -> String

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

Totality: total
Visibility: public export

join : String -> Foldable t => t String -> String

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

Totality: total
Visibility: public export

index : Nat -> String -> Maybe Char

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

Totality: total
Visibility: public export

indentLines : Nat -> String -> String

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

Totality: total
Visibility: public export

justifyLeft : Nat -> Char -> String -> String

  Left-justify a string to the given length, using the
  specified fill character on the right.

Totality: total
Visibility: export

justifyRight : Nat -> Char -> String -> String

  Right-justify a string to the given length, using the
  specified fill character on the left.

Totality: total
Visibility: export