@@ -73,3 +73,16 @@ index n str with (unpack str)
73 index n str | [] = Nothing
73 index n str | [] = Nothing
74 index Z str | (x :: xs) = Just x
74 index Z str | (x :: xs) = Just x
75 index (S n) str | (x :: xs) = index n str | xs
75 index (S n) str | (x :: xs) = index n str | xs
77+||| Produce a string by repeating the character `c` `n` times.
78+replicate : (n : Nat) -> (c : Char) -> String
79+replicate n c = pack $ replicate n c
81+||| Indent a given string by `n` spaces.
82+indent : (n : Nat) -> String -> String
83+indent n x = replicate n ' ' ++ x
85+||| Indent each line of a given string by `n` spaces.
86+indentLines : (n : Nat) -> String -> String
87+indentLines n str = unlines $ map (indent n) $ lines str