Data.Pair0

Definitions

record Pair0 : Type -> Type -> Type

  A pair of two erased values.

Totality: total
Visibility: public export
Constructor: 

P0 : (0 _ : a) -> (0 _ : b) -> Pair0 a b

Projections:

0 .fst : Pair0 a b -> a

0 .snd : Pair0 a b -> b

0 .fst : Pair0 a b -> a

Totality: total
Visibility: public export

0 fst : Pair0 a b -> a

Totality: total
Visibility: public export

0 .snd : Pair0 a b -> b

Totality: total
Visibility: public export

0 snd : Pair0 a b -> b

Totality: total
Visibility: public export

bimap : (0 _ : (a -> c)) -> (0 _ : (b -> d)) -> Pair0 a b -> Pair0 c d

  This is the identity at runtime.

Totality: total
Visibility: public export

map : (0 _ : (b -> d)) -> Pair0 a b -> Pair0 a d

Totality: total
Visibility: public export