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

Safe Haskell | None

Agda.Utils.Tuple

Contents

- Triple (stolen from Data.Tuple.HT)

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
- 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)
- newtype List2 a = List2 {
  - list2 :: (a, a)
  }

# Documentation

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

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)

Lifted pairing.

# Triple (stolen from Data.Tuple.HT)

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

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

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

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 |
Foldable List2 |
Traversable List2 |
Eq a => Eq (List2 a) |