From d76b58360ede2b0c983ac6ef14fc8d841a4973a7 Mon Sep 17 00:00:00 2001
From: David Raymond Christiansen <david@davidchristiansen.dk>
Date: Wed, 12 Aug 2015 22:28:49 -0700
Subject: [PATCH] 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.
---
 libs/prelude/Prelude/Applicative.idr | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/libs/prelude/Prelude/Applicative.idr b/libs/prelude/Prelude/Applicative.idr
index 5e8102bfb..aff7c95be 100644
--- a/libs/prelude/Prelude/Applicative.idr
+++ b/libs/prelude/Prelude/Applicative.idr
@@ -5,6 +5,7 @@ import Builtins
 import Prelude.Basics
 import Prelude.Bool
 import Prelude.Classes
+import Prelude.Foldable
 import Prelude.Functor
 
 ---- Applicative functors/Idioms
@@ -48,3 +49,9 @@ guard a = if a then pure () else empty
 when : Applicative f => Bool -> Lazy (f ()) -> f ()
 when True f = Force f
 when False f = pure ()
+
+||| Fold using Alternative
+|||
+||| This is called `asum` in Haskell.
+choice : (Foldable t, Alternative f) => t (f a) -> f a
+choice x = foldr (<|>) empty x