module Data.String.Extra import Data.Strings %default total  infixl 5 +>infixr 5 <+ ||| Adds a character to the end of the specified string.|||||| ```idris example||| strSnoc "AB" 'C'||| ```||| ```idris example||| strSnoc "" 'A'||| ```public exportstrSnoc : String -> Char -> StringstrSnoc s c = s ++ (singleton c) ||| Alias of `strSnoc`|||||| ```idris example||| "AB" +> 'C'||| ```public export(+>) : String -> Char -> String(+>) = strSnoc ||| Alias of `strCons`|||||| ```idris example||| 'A' <+ "AB"||| ```public export(<+) : Char -> String -> String(<+) = strCons ||| Take the first `n` characters from a string. Returns the whole string||| if it's too short.public exporttake : (n : Nat) -> (input : String) -> Stringtake n str = substr Z n str ||| Take the last `n` characters from a string. Returns the whole string||| if it's too short.public exporttakeLast : (n : Nat) -> (input : String) -> StringtakeLast n str with (length str)  takeLast n str | len with (isLTE n len)    takeLast n str | len | Yes prf = substr (len `minus` n) len str    takeLast n str | len | No contra = str ||| Remove the first `n` characters from a string. Returns the empty string if||| the input string is too short.public exportdrop : (n : Nat) -> (input : String) -> Stringdrop n str = substr n (length str) str ||| Remove the last `n` characters from a string. Returns the empty string if||| the input string is too short.public exportdropLast : (n : Nat) -> (input : String) -> StringdropLast n str = reverse (drop n (reverse str)) ||| Remove the first and last `n` characters from a string. Returns the empty||| string if the input string is too short.public exportshrink : (n : Nat) -> (input : String) -> Stringshrink n str = dropLast n (drop n str) ||| Concatenate the strings from a `Foldable` containing strings, separated by||| the given string.public exportjoin : (sep : String) -> Foldable t => (xs : t String) -> Stringjoin sep xs = drop (length sep)                   (foldl (\acc, x => acc ++ sep ++ x) "" xs) ||| Get a character from a string if the string is long enough.public exportindex : (n : Nat) -> (input : String) -> Maybe Charindex n str with (unpack str)  index n str | [] = Nothing  index Z str | (x :: xs) = Just x  index (S n) str | (x :: xs) = index n str | xs ||| Produce a string by repeating the character `c` `n` times.public exportreplicate : (n : Nat) -> (c : Char) -> Stringreplicate n c = pack $ replicate n c ||| Indent a given string by `n` spaces.public exportindent : (n : Nat) -> String -> Stringindent n x = replicate n ' ' ++ x ||| Indent each line of a given string by `n` spaces.public exportindentLines : (n : Nat) -> String -> StringindentLines n str = unlines $ map (indent n) $ lines str