on master help sign in
Add "choice"
d76b583David Raymond Christiansen
libs/prelude/Prelude/Applicative.idr+7
@@ -5,6 +5,7 @@ import Builtins
5import Prelude.Basics
5import Prelude.Basics
6import Prelude.Bool
6import Prelude.Bool
7import Prelude.Classes
7import Prelude.Classes
8+import Prelude.Foldable
8import Prelude.Functor
9import Prelude.Functor
9
10
10---- Applicative functors/Idioms
11---- Applicative functors/Idioms
@@ -48,3 +49,9 @@ guard a = if a then pure () else empty
48when : Applicative f => Bool -> Lazy (f ()) -> f ()
49when : Applicative f => Bool -> Lazy (f ()) -> f ()
49when True f = Force f
50when True f = Force f
50when False f = pure ()
51when False f = pure ()
52+
53+||| Fold using Alternative
54+|||
55+||| This is called `asum` in Haskell.
56+choice : (Foldable t, Alternative f) => t (f a) -> f a
57+choice x = foldr (<|>) empty x