idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-17 08:11:45 +03:00
Code Issues Projects Releases Wiki Activity

Move hand specialised foldlC into Core.Core

Browse Source
This commit is contained in:
Johann Rudloff 2021-04-26 09:12:44 +02:00
parent 881a5e7fbc
commit 1afece45c5
2 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Core/Core.idr
View File

@ -566,6 +566,11 @@ Catchable Core Error where
Right val => pure (Right val))
throw = coreFail
-- Prelude.Monad.foldlM hand specialised for Core
export
foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a
foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)
-- Traversable (specialised)
traverse' : (a -> Core b) -> List a -> List b -> Core (List b)
traverse' f [] acc = pure (reverse acc)

4
src/Idris/Package.idr
View File

@ -415,10 +415,6 @@ bitraverseC f g (This a) = [| This (f a) |]
bitraverseC f g (That b) = [| That (g b) |]
bitraverseC f g (Both a b) = [| Both (f a) (g b) |]
-- Prelude.Monad.foldlM hand specialised for Core
foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a
foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)
-- Data.StringTrie.foldWithKeysM hand specialised for Core
foldWithKeysC : Monoid b => (List String -> Core b) -> (List String -> a -> Core b) -> StringTrie a -> Core b
foldWithKeysC {a} {b} fk fv = go []