idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

[ new ] mapWithKey for name maps

Browse Source
This commit is contained in:
Justus Matthiesen 2023-02-06 17:11:07 +00:00 committed by G. Allais
parent eaa6c8b6d7
commit 9bdc875b79
1 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/Libraries/Data/NameMap.idr
View File

@ -291,6 +291,17 @@ implementation Functor NameMap where
map _ Empty = Empty
map f (M n t) = M _ (treeMap f t)
treeMapWithKey : (Name -> a -> b) -> Tree n a -> Tree n b
treeMapWithKey f (Leaf k v) = Leaf k (f k v)
treeMapWithKey f (Branch2 t1 k t2) = Branch2 (treeMapWithKey f t1) k (treeMapWithKey f t2)
treeMapWithKey f (Branch3 t1 k1 t2 k2 t3)
= Branch3 (treeMapWithKey f t1) k1 (treeMapWithKey f t2) k2 (treeMapWithKey f t3)
export
mapWithKey : (Name -> a -> b) -> NameMap a -> NameMap b
mapWithKey f Empty = Empty
mapWithKey f (M n t) = M _ (treeMapWithKey f t)
||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
||| Uses the ordering of the first map given.
export