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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Three

Description

Tools for 3-way partitioning.

Synopsis

- data Three
  - = One
  - | Two
  - | Three
- partition3 :: (a -> Three) -> [a] -> ([a], [a], [a])
- data Either3 a b c
  - = In1 a
  - | In2 b
  - | In3 c
- partitionEithers3 :: [Either3 a b c] -> ([a], [b], [c])
- mapEither3M :: Applicative m => (a -> m (Either3 b c d)) -> [a] -> m ([b], [c], [d])
- forEither3M :: Applicative m => [a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])

# 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 Methods minBound :: Three Source # maxBound :: Three Source #
Enum Three Source # |
Instance details Defined in Agda.Utils.Three Methods succ :: Three -> Three Source # pred :: Three -> Three Source # toEnum :: Int -> Three Source # fromEnum :: Three -> Int Source # enumFrom :: Three -> [Three] Source # enumFromThen :: Three -> Three -> [Three] Source # enumFromTo :: Three -> Three -> [Three] Source # enumFromThenTo :: Three -> Three -> Three -> [Three] Source #
Show Three Source # |
Instance details Defined in Agda.Utils.Three Methods showsPrec :: Int -> Three -> ShowS Source # show :: Three -> String Source # showList :: [Three] -> ShowS Source #
Eq Three Source # |
Instance details Defined in Agda.Utils.Three Methods (==) :: Three -> Three -> Bool Source # (/=) :: Three -> Three -> Bool Source #
Ord Three Source # |
Instance details Defined in Agda.Utils.Three Methods compare :: Three -> Three -> Ordering Source # (<) :: Three -> Three -> Bool Source # (<=) :: Three -> Three -> Bool Source # (>) :: Three -> Three -> Bool Source # (>=) :: Three -> Three -> Bool Source # max :: Three -> Three -> Three Source # min :: Three -> Three -> Three Source #

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 Source # show :: Either3 a b c -> String Source # showList :: [Either3 a b c] -> ShowS Source #
(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 Source # (/=) :: Either3 a b c -> Either3 a b c -> Bool Source #
(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 Source #

(<) :: Either3 a b c -> Either3 a b c -> Bool Source #

(<=) :: Either3 a b c -> Either3 a b c -> Bool Source #

(>) :: Either3 a b c -> Either3 a b c -> Bool Source #

(>=) :: Either3 a b c -> Either3 a b c -> Bool Source #

max :: Either3 a b c -> Either3 a b c -> Either3 a b c Source #

min :: Either3 a b c -> Either3 a b c -> Either3 a b c Source #

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 #