From 6fe8dc2a024e5ec7d389a3e738bae0c316a3a7f6 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 11 Feb 2024 14:16:42 -0800 Subject: [PATCH] Add an 'iterate' function to Utils Signed-off-by: Danila Fedorin --- Utils.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Utils.agda b/Utils.agda index a8f9b64..9156f3b 100644 --- a/Utils.agda +++ b/Utils.agda @@ -1,5 +1,6 @@ module Utils where +open import Data.Nat using (ℕ; suc) open import Data.List using (List; []; _∷_; _++_) open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Unary.All using (All; []; _∷_; map) @@ -34,3 +35,7 @@ All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs All-x∈xs : ∀ {a} {A : Set a} (xs : List A) → All (λ x → x ∈ xs) xs All-x∈xs [] = [] All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs') + +iterate : ∀ {a} {A : Set a} (n : ℕ) → (f : A → A) → A → A +iterate 0 _ a = a +iterate (suc n) f a = f (iterate n f a)