module Data.Fin.List (Peano, List (..),
fromList, uncons, head, tail, init, last, reverse, rotate, at, swap, (!!), findIndex) where
import Prelude ()
import Data.Bool (Bool, bool)
import Control.Applicative
import Control.Category (id)
import Data.Fin.Private as Fin
import Data.Peano (Peano)
findIndex :: Alternative p => (a -> Bool) -> List n a -> p (Fin n)
findIndex :: (a -> Bool) -> List n a -> p (Fin n)
findIndex p :: a -> Bool
p = \ case
Nil -> p (Fin n)
forall (f :: * -> *) a. Alternative f => f a
empty
a :: a
a:.as :: List n a
as -> (p (Fin ('Succ n)) -> p (Fin ('Succ n)))
-> (p (Fin ('Succ n)) -> p (Fin ('Succ n)))
-> Bool
-> p (Fin ('Succ n))
-> p (Fin n)
forall a. a -> a -> Bool -> a
bool p (Fin ('Succ n)) -> p (Fin ('Succ n))
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (Fin ('Succ n) -> p (Fin ('Succ n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Fin ('Succ n)
forall (n :: Peano). Fin ('Succ n)
Zero p (Fin ('Succ n)) -> p (Fin ('Succ n)) -> p (Fin ('Succ n))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>) (a -> Bool
p a
a) (Fin n -> Fin ('Succ n)
forall (n :: Peano). Fin n -> Fin ('Succ n)
Succ (Fin n -> Fin ('Succ n)) -> p (Fin n) -> p (Fin ('Succ n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Bool) -> List n a -> p (Fin n)
forall (p :: * -> *) a (n :: Peano).
Alternative p =>
(a -> Bool) -> List n a -> p (Fin n)
findIndex a -> Bool
p List n a
as)