Agda-2.6.2.2.20221106: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.Three

Description

Tools for 3-way partitioning.

Synopsis

Documentation

data Three Source #

Enum type with 3 elements.

Constructors

One 
Two 
Three 

Instances

Instances details
Bounded Three Source # 
Instance details

Defined in Agda.Utils.Three

Enum Three Source # 
Instance details

Defined in Agda.Utils.Three

Show Three Source # 
Instance details

Defined in Agda.Utils.Three

Methods

showsPrec :: Int -> Three -> ShowS #

show :: Three -> String #

showList :: [Three] -> ShowS #

Eq Three Source # 
Instance details

Defined in Agda.Utils.Three

Methods

(==) :: Three -> Three -> Bool #

(/=) :: Three -> Three -> Bool #

Ord Three Source # 
Instance details

Defined in Agda.Utils.Three

Methods

compare :: Three -> Three -> Ordering #

(<) :: Three -> Three -> Bool #

(<=) :: Three -> Three -> Bool #

(>) :: Three -> Three -> Bool #

(>=) :: Three -> Three -> Bool #

max :: Three -> Three -> Three #

min :: Three -> Three -> Three #

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

Instances details
(Show a, Show b, Show c) => Show (Either3 a b c) Source # 
Instance details

Defined in Agda.Utils.Three

Methods

showsPrec :: Int -> Either3 a b c -> ShowS #

show :: Either3 a b c -> String #

showList :: [Either3 a b c] -> ShowS #

(Eq a, Eq b, Eq c) => Eq (Either3 a b c) Source # 
Instance details

Defined 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 details

Defined in Agda.Utils.Three

Methods

compare :: 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 #

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 #