ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.Tuple

value(-*-) :: (a -> c) -> (b -> d) -> (a, b) -> (c, d)

Bifunctoriality for pairs.

valuemapFst :: (a -> c) -> (a, b) -> (c, b)

mapFst f = f -*- id

valuemapSnd :: (b -> d) -> (a, b) -> (a, d)

mapSnd g = id -*- g

value(/\) :: (a -> b) -> (a -> c) -> a -> (b, c)

Lifted pairing.

valuefst3 :: (a, b, c) -> a

valuesnd3 :: (a, b, c) -> b

valuethd3 :: (a, b, c) -> c

valueswap :: (a, b) -> (b, a)

Swap the components of a pair.

valueuncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d

valueuncurry4 :: (a -> b -> c -> d -> e) -> (a, b, c, d) -> e

valuemapPairM :: Applicative m => (a -> m c) -> (b -> m d) -> (a, b) -> m (c, d)

Monadic version of -*-.

valuemapFstM :: Functor m => (a -> m c) -> (a, b) -> m (c, b)

Monadic mapFst.

valuemapSndM :: Functor m => (b -> m d) -> (a, b) -> m (a, d)

Monadic mapSnd.

datadata Pair a

Instances5Functor, Applicative, Foldable, Traversable, Eq