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

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Tuple

Contents

Synopsis

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.

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

Swap. (Only in Data.Tuple from base-4.3)

Triple (stolen from Data.Tuple.HT)

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

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

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

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.

newtype List2 a Source

Constructors

List2 

Fields

list2 :: (a, a)