Agda-2.6.3.20230930: 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 #