From 12305cc232f669be4a519530893d1ba9b570b681 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 20 Jan 2025 00:07:50 -0500 Subject: [PATCH] Add repeatN to Util --- src/Util.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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