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 Declarations:
infixl operator, level 5
infixl operator, level 5

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

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

Totality: total
Visibility: public export
Fixity Declarations:
infixr operator, level 5
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

leftEllipsis : Nat -> String -> String -> String

  Truncates a string to the given length.
  If the given string is longer, replace first characters with given prefix.
  
  Say, `leftEllipsis 5 ".." "abcdefgh"` should give `"..fgh"` and
  `leftEllipsis 5 "" "abcdefgh"` should give `"defgh"`.
  
  Notice, that the resulting string can be longer than max length if the prefix is longer.

Totality: total
Visibility: export

rightEllipsis : Nat -> String -> String -> String

  Truncates a string to the given length.
  If the given string is longer, replace last characters with given suffix.
  
  Say, `rightEllipsis 5 ".." "abcdefgh"` should give `"abc.."` and
  `rightEllipsis 5 "" "abcdefgh"` should give `"abcde"`.
  
  Notice, that the resulting string can be longer than max length if the suffix is longer.

Totality: total
Visibility: export