Idris/advent
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

Add repeatN to Util

Browse source
This commit is contained in:
Nathan McCarty 2025-01-20 00:07:50 -05:00
parent fe4a20ade6
commit 12305cc232
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Util.md
View file

@ -13,6 +13,19 @@ import Data.List.Lazy
%default total %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 ## Either
<!-- idris <!-- idris