Agda-2.6.0: A dependently typed functional programming language and proof assistant

Agda.Utils.Three

Description

Tools for 3-way partitioning.

Synopsis

# Documentation

data Three Source #

Enum type with 3 elements.

Constructors

 One Two Three
Instances
 Source # Instance detailsDefined in Agda.Utils.Three Methods Source # Instance detailsDefined in Agda.Utils.Three Methodssucc :: Three -> Three #pred :: Three -> Three #toEnum :: Int -> Three #enumFrom :: Three -> [Three] #enumFromThen :: Three -> Three -> [Three] #enumFromTo :: Three -> Three -> [Three] #enumFromThenTo :: Three -> Three -> Three -> [Three] # Source # Instance detailsDefined in Agda.Utils.Three Methods(==) :: Three -> Three -> Bool #(/=) :: Three -> Three -> Bool # Source # Instance detailsDefined in Agda.Utils.Three Methods(<) :: Three -> Three -> Bool #(<=) :: Three -> Three -> Bool #(>) :: Three -> Three -> Bool #(>=) :: Three -> Three -> Bool #max :: Three -> Three -> Three #min :: Three -> Three -> Three # Source # Instance detailsDefined in Agda.Utils.Three MethodsshowsPrec :: Int -> Three -> ShowS #show :: Three -> String #showList :: [Three] -> ShowS #

partition3 :: (a -> Three) -> [a] -> ([a], [a], [a]) Source #

Partition a list into 3 groups.

Preserves the relative order or elements.

data Either3 a b c Source #

Disjoint sum of three.

Constructors

 In1 a In2 b In3 c
Instances
 (Eq a, Eq b, Eq c) => Eq (Either3 a b c) Source # Instance detailsDefined in Agda.Utils.Three Methods(==) :: Either3 a b c -> Either3 a b c -> Bool #(/=) :: Either3 a b c -> Either3 a b c -> Bool # (Ord a, Ord b, Ord c) => Ord (Either3 a b c) Source # Instance detailsDefined in Agda.Utils.Three Methodscompare :: Either3 a b c -> Either3 a b c -> Ordering #(<) :: Either3 a b c -> Either3 a b c -> Bool #(<=) :: Either3 a b c -> Either3 a b c -> Bool #(>) :: Either3 a b c -> Either3 a b c -> Bool #(>=) :: Either3 a b c -> Either3 a b c -> Bool #max :: Either3 a b c -> Either3 a b c -> Either3 a b c #min :: Either3 a b c -> Either3 a b c -> Either3 a b c # (Show a, Show b, Show c) => Show (Either3 a b c) Source # Instance detailsDefined in Agda.Utils.Three MethodsshowsPrec :: Int -> Either3 a b c -> ShowS #show :: Either3 a b c -> String #showList :: [Either3 a b c] -> ShowS #

partitionEithers3 :: [Either3 a b c] -> ([a], [b], [c]) Source #

Partition a list into 3 groups.

Preserves the relative order or elements.

mapEither3M :: Applicative m => (a -> m (Either3 b c d)) -> [a] -> m ([b], [c], [d]) Source #

forEither3M :: Applicative m => [a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d]) Source #