From 79f5c75fd170bd1b267cef87e02aafdc848e24be Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 15:38:02 +0800 Subject: [PATCH] Add the mapi function I'm unsure if we can add this to a trait or not --- Stdlib/Data/List/Base.juvix | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 4304d3ef..b52ad407 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -57,6 +57,16 @@ listMap {A B} (fun : A -> B) : (list : List A) -> List B | nil := nil | (h :: hs) := fun h :: listMap fun hs; +--- 𝒪(𝓃). Maps a function over each element of a ;List; with an index. +{-# specialize: [1] #-} +mapi {A B} : (fun : Nat -> A -> B) -> List A -> List B + | fun xs := + let + go : Nat -> List A -> List B + | _ nil := nil + | n (x :: xs) := fun n x :: go (suc n) xs; + in go zero xs; + syntax iterator filter {init := 0; range := 1}; --- 𝒪(𝓃). Filters a ;List; according to a given predicate, i.e.,