diff --git a/src/Util.md b/src/Util.md index 836a4cd..62d4a83 100644 --- a/src/Util.md +++ b/src/Util.md @@ -13,6 +13,19 @@ import Data.List.Lazy %default total ``` +## Functions + +### repeatN + +Recursively applies `f` to `seed` N times + +```idris +export +repeatN : (times : Nat) -> (f : a -> a) -> (seed : a) -> a +repeatN 0 f seed = seed +repeatN (S times') f seed = repeatN times' f (f seed) +``` + ## Either