on master help sign in
Add "choice"

This is called asum in Haskell. I think it's appropriate for the Prelude because I've defined it myself on a number of occasions.

commitd76b58360ede2b0c983ac6ef14fc8d841a4973a7 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 12 Aug 2015, 22:28 (11 years ago) parent030da05
1 file changed+7
libs/prelude/Prelude/Applicative.idr+7
libs/prelude/Prelude/Applicative.idr+7
@@ -5,6 +5,7 @@ import Builtins
55import Prelude.Basics
66import Prelude.Bool
77import Prelude.Classes
8+import Prelude.Foldable
89import Prelude.Functor
910
1011---- Applicative functors/Idioms
@@ -48,3 +49,9 @@ guard a = if a then pure () else empty
4849when : Applicative f => Bool -> Lazy (f ()) -> f ()
4950when True f = Force f
5051when 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