
  0 | module Syntax.Monad.Logic
  1 | 
  2 | import public Language.Implicits.IfUnsolved
  3 | 
  4 | %default total
  5 | 
  6 | -- Monadically lazy on the second argument
  7 | public export
  8 | (&&) : Monad m => m Bool -> m Bool -> m Bool
  9 | l && r = do
 10 |   True <- l
 11 |     | False => pure False
 12 |   r
 13 | 
 14 | -- Monadically lazy on the second argument
 15 | public export
 16 | (||) : Monad m => m Bool -> m Bool -> m Bool
 17 | l || r = do
 18 |   False <- l
 19 |     | True => pure True
 20 |   r
 21 | 
 22 | public export %inline
 23 | all : Monad n => Foldable f => Functor f => (0 _ : IfUnsolved f List) =>
 24 |       (a -> n Bool) -> f a -> n Bool
 25 | all = foldl (&&) (pure True) .: map
 26 | 
 27 | public export %inline
 28 | any : Monad n => Foldable f => Functor f => (0 _ : IfUnsolved f List) =>
 29 |       (a -> n Bool) -> f a -> n Bool
 30 | any = foldl (||) (pure False) .: map
 31 |