Agda.Utils.Tuple

Documentation

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

Bifunctoriality for pairs.

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

mapFst f = f -*- id

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

mapSnd g = id -*- g

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

Lifted pairing.

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

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

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

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

Swap the components of a pair.

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)

Monadic version of -*-.

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

Monadic mapFst.

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

Monadic mapSnd.

newtype List2 a

Constructors

List2

Fields

• list2 :: (a, a)

Instances

Functor List2

Defined in Agda.Utils.Tuple

Methods

fmap :: (a -> b) -> List2 a -> List2 b

(<$) :: a -> List2 b -> List2 a

Applicative List2

Defined in Agda.Utils.Tuple

Methods

pure :: a -> List2 a

(<*>) :: List2 (a -> b) -> List2 a -> List2 b

liftA2 :: (a -> b -> c) -> List2 a -> List2 b -> List2 c

(*>) :: List2 a -> List2 b -> List2 b

(<*) :: List2 a -> List2 b -> List2 a

Foldable List2

Defined in Agda.Utils.Tuple

Methods

fold :: Monoid m => List2 m -> m

foldMap :: Monoid m => (a -> m) -> List2 a -> m

foldMap' :: Monoid m => (a -> m) -> List2 a -> m

foldr :: (a -> b -> b) -> b -> List2 a -> b

foldr' :: (a -> b -> b) -> b -> List2 a -> b

foldl :: (b -> a -> b) -> b -> List2 a -> b

foldl' :: (b -> a -> b) -> b -> List2 a -> b

foldr1 :: (a -> a -> a) -> List2 a -> a

foldl1 :: (a -> a -> a) -> List2 a -> a

toList :: List2 a -> [a]

null :: List2 a -> Bool

length :: List2 a -> Int

elem :: Eq a => a -> List2 a -> Bool

maximum :: Ord a => List2 a -> a

minimum :: Ord a => List2 a -> a

sum :: Num a => List2 a -> a

product :: Num a => List2 a -> a

Traversable List2

Defined in Agda.Utils.Tuple

Methods

traverse :: Applicative f => (a -> f b) -> List2 a -> f (List2 b)

sequenceA :: Applicative f => List2 (f a) -> f (List2 a)

mapM :: Monad m => (a -> m b) -> List2 a -> m (List2 b)

sequence :: Monad m => List2 (m a) -> m (List2 a)

Eq a => Eq (List2 a)

Defined in Agda.Utils.Tuple

Methods

(==) :: List2 a -> List2 a -> Bool

(/=) :: List2 a -> List2 a -> Bool