Agda

Safe Haskell	None
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)
sortPair :: Ord a => (a, a) -> (a, a)
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 :: Functor m => (a -> m c) -> (a, b) -> m (c, b)
mapSndM :: Functor 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.

sortPair :: Ord a => (a, a) -> (a, a) Source #

Order a pair.

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

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

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

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

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 :: Functor m => (a -> m c) -> (a, b) -> m (c, b) Source #

Monadic mapFst.

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

Monadic mapSnd.

data Pair a Source #

Constructors

Pair a a

Instances

Instances details

Applicative Pair Source #

Instance details

Defined in Agda.Utils.Tuple

Methods

pure :: a -> Pair a #

(<*>) :: Pair (a -> b) -> Pair a -> Pair b #

liftA2 :: (a -> b -> c) -> Pair a -> Pair b -> Pair c #

(*>) :: Pair a -> Pair b -> Pair b #

(<*) :: Pair a -> Pair b -> Pair a #

Functor Pair Source #

Instance details

Defined in Agda.Utils.Tuple

Methods

fmap :: (a -> b) -> Pair a -> Pair b #

(<$) :: a -> Pair b -> Pair a #

Foldable Pair Source #

Instance details

Defined in Agda.Utils.Tuple

Methods

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

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

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

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

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

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

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

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

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

toList :: Pair a -> [a] #

null :: Pair a -> Bool #

length :: Pair a -> Int #

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

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

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

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

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

Traversable Pair Source #

Instance details

Defined in Agda.Utils.Tuple

Methods

traverse :: Applicative f => (a -> f b) -> Pair a -> f (Pair b) #

sequenceA :: Applicative f => Pair (f a) -> f (Pair a) #

mapM :: Monad m => (a -> m b) -> Pair a -> m (Pair b) #

sequence :: Monad m => Pair (m a) -> m (Pair a) #

NFData a => NFData (Pair a) Source #

Instance details

Defined in Agda.Utils.Tuple

Methods

rnf :: Pair a -> () #

Generic (Pair a) Source #

Instance details

Defined in Agda.Utils.Tuple

Associated Types

type Rep (Pair a)
Instance details Defined in Agda.Utils.Tuple type Rep (Pair a) = D1 ('MetaData "Pair" "Agda.Utils.Tuple" "Agda-2.8.0-inplace" 'False) (C1 ('MetaCons "Pair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Methods

from :: Pair a -> Rep (Pair a) x #

to :: Rep (Pair a) x -> Pair a #

Show a => Show (Pair a) Source #

Instance details

Defined in Agda.Utils.Tuple

Methods

showsPrec :: Int -> Pair a -> ShowS #

show :: Pair a -> String #

showList :: [Pair a] -> ShowS #

Eq a => Eq (Pair a) Source #

Instance details

Defined in Agda.Utils.Tuple

Methods

(==) :: Pair a -> Pair a -> Bool #

(/=) :: Pair a -> Pair a -> Bool #

type Rep (Pair a) Source #

Instance details

Defined in Agda.Utils.Tuple

type Rep (Pair a) = D1 ('MetaData "Pair" "Agda.Utils.Tuple" "Agda-2.8.0-inplace" 'False) (C1 ('MetaCons "Pair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))