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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.Tuple

Synopsis

- (-*-) :: (a -> c) -> (b -> d) -> (a, b) -> (c, d)
- mapFst :: (a -> c) -> (a, b) -> (c, b)
- mapSnd :: (b -> d) -> (a, b) -> (a, d)
- (/\) :: (a -> b) -> (a -> c) -> a -> (b, c)
- fst3 :: (a, b, c) -> a
- snd3 :: (a, b, c) -> b
- thd3 :: (a, b, c) -> c
- swap :: (a, b) -> (b, a)
- uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
- uncurry4 :: (a -> b -> c -> d -> e) -> (a, b, c, d) -> e
- mapPairM :: Applicative m => (a -> m c) -> (b -> m d) -> (a, b) -> m (c, d)
- mapFstM :: Applicative m => (a -> m c) -> (a, b) -> m (c, b)
- mapSndM :: Applicative m => (b -> m d) -> (a, b) -> m (a, d)
- data Pair a = Pair a a

# Documentation

(-*-) :: (a -> c) -> (b -> d) -> (a, b) -> (c, d) infix 2 Source #

Bifunctoriality for pairs.

mapFst :: (a -> c) -> (a, b) -> (c, b) Source #

    mapFst f = f -*- id

mapSnd :: (b -> d) -> (a, b) -> (a, d) Source #

    mapSnd g = id -*- g

(/\) :: (a -> b) -> (a -> c) -> a -> (b, c) infix 3 Source #

Lifted pairing.

fst3 :: (a, b, c) -> a Source #

snd3 :: (a, b, c) -> b Source #

thd3 :: (a, b, c) -> c Source #

swap :: (a, b) -> (b, a) Source #

Swap the components of a pair.

uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d Source #

uncurry4 :: (a -> b -> c -> d -> e) -> (a, b, c, d) -> e Source #

mapPairM :: Applicative m => (a -> m c) -> (b -> m d) -> (a, b) -> m (c, d) Source #

Monadic version of `-*-`.

mapFstM :: Applicative m => (a -> m c) -> (a, b) -> m (c, b) Source #

Monadic `mapFst`.

mapSndM :: Applicative m => (b -> m d) -> (a, b) -> m (a, d) Source #

Monadic `mapSnd`.

data Pair a Source #

Constructors

Pair a a |

#### Instances

Instances details

Foldable Pair Source # |

Instance details

Defined in Agda.Utils.Tuple

Methods

fold :: Monoid m => Pair m -> m Source #

foldMap :: Monoid m => (a -> m) -> Pair a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Pair a -> m Source #

foldr :: (a -> b -> b) -> b -> Pair a -> b Source #

foldr' :: (a -> b -> b) -> b -> Pair a -> b Source #

foldl :: (b -> a -> b) -> b -> Pair a -> b Source #

foldl' :: (b -> a -> b) -> b -> Pair a -> b Source #

foldr1 :: (a -> a -> a) -> Pair a -> a Source #

foldl1 :: (a -> a -> a) -> Pair a -> a Source #

toList :: Pair a -> [a] Source #

null :: Pair a -> Bool Source #

length :: Pair a -> Int Source #

elem :: Eq a => a -> Pair a -> Bool Source #

maximum :: Ord a => Pair a -> a Source #

minimum :: Ord a => Pair a -> a Source #

sum :: Num a => Pair a -> a Source #

product :: Num a => Pair a -> a Source #

Traversable Pair Source # |
Instance details Defined in Agda.Utils.Tuple Methods traverse :: Applicative f => (a -> f b) -> Pair a -> f (Pair b) Source # sequenceA :: Applicative f => Pair (f a) -> f (Pair a) Source # mapM :: Monad m => (a -> m b) -> Pair a -> m (Pair b) Source # sequence :: Monad m => Pair (m a) -> m (Pair a) Source #
Applicative Pair Source # |
Instance details Defined in Agda.Utils.Tuple Methods pure :: a -> Pair a Source # (<*>) :: Pair (a -> b) -> Pair a -> Pair b Source # liftA2 :: (a -> b -> c) -> Pair a -> Pair b -> Pair c Source # (*>) :: Pair a -> Pair b -> Pair b Source # (<*) :: Pair a -> Pair b -> Pair a Source #
Functor Pair Source # |
Instance details Defined in Agda.Utils.Tuple Methods fmap :: (a -> b) -> Pair a -> Pair b Source # (<$) :: a -> Pair b -> Pair a Source #
Eq a => Eq (Pair a) Source # |
Instance details Defined in Agda.Utils.Tuple Methods (==) :: Pair a -> Pair a -> Bool Source # (/=) :: Pair a -> Pair a -> Bool Source #