IdrisDoc: Prelude.Pairs

Prelude.Pairs

swap : (a, b) -> (b, a)
data Subset : (a : Type) -> (P : a -> Type) -> Type

Dependent pair where the second field is erased.

Element : (x : a) -> (pf : P x) -> Subset a P
data Exists : (P : a -> Type) -> Type

Dependent pair where the first field is erased.

Evidence : (x : a) -> (pf : P x) -> Exists P