strRepeat : Nat -> String -> String strRepeat Z s = "" strRepeat (S n) s = s ++ strRepeat n s chrRepeat : Nat -> Char -> String chrRepeat Z c = "" chrRepeat (S n) c = strCons c $ chrRepeat n c