
  0 | module Data.Pair0
  1 | 
  2 | %default total
  3 | 
  4 | ||| A pair of two erased values.
  5 | public export
  6 | record Pair0 (a,b : Type) where
  7 |   constructor P0
  8 |   0 fst : a
  9 |   0 snd : b
 10 | 
 11 | ||| This is the identity at runtime.
 12 | public export
 13 | bimap : (0 f : a -> c) -> (0 g : b -> d) -> Pair0 a b -> Pair0 c d
 14 | bimap f g (P0 x y) = P0 (f x) (g y)
 15 | 
 16 | public export %inline
 17 | map : (0 f : b -> d) -> Pair0 a b -> Pair0 a d
 18 | map = bimap id
 19 |