@@ -29,3 +29,44 @@ strSnoc s c = s ++ (singleton c)
2929||| ```
3030(<+) : Char -> String -> String
3131(<+) = strCons
32+
33+||| Take the first `n` characters from a string. Returns the whole string
34+||| if it's too short.
35+take : (n : Nat) -> (input : String) -> String
36+take n str = substr Z n str
37+
38+||| Take the last `n` characters from a string. Returns the whole string
39+||| if it's too short.
40+takeLast : (n : Nat) -> (input : String) -> String
41+takeLast n str with (length str)
42+ takeLast n str | len with (isLTE n len)
43+ takeLast n str | len | Yes prf = substr (len - n) len str
44+ takeLast n str | len | No contra = str
45+
46+||| Remove the first `n` characters from a string. Returns the empty string if
47+||| the input string is too short.
48+drop : (n : Nat) -> (input : String) -> String
49+drop n str = substr n (length str) str
50+
51+||| Remove the last `n` characters from a string. Returns the empty string if
52+||| the input string is too short.
53+dropLast : (n : Nat) -> (input : String) -> String
54+dropLast n str = reverse (drop n (reverse str))
55+
56+||| Remove the first and last `n` characters from a string. Returns the empty
57+||| string if the input string is too short.
58+shrink : (n : Nat) -> (input : String) -> String
59+shrink n str = dropLast n (drop n str)
60+
61+||| Concatenate the strings from a `Foldable` containing strings, separated by
62+||| the given string.
63+join : (sep : String) -> Foldable t => (xs : t String) -> String
64+join sep xs = drop (length sep)
65+ (foldl (\acc, x => acc ++ sep ++ x) "" xs)
66+
67+||| Get a character from a string if the string is long enough.
68+index : (n : Nat) -> (input : String) -> Maybe Char
69+index n str with (unpack str)
70+ index n str | [] = Nothing
71+ index Z str | (x :: xs) = Just x
72+ index (S n) str | (x :: xs) = index n str | xs