IdrisDoc: Builtins

Builtins

data UPair : (A : AnyType) -> (B : AnyType) -> AnyType

The non-dependent pair type, also known as conjunction, usable with
UniqueTypes.

A

the type of the left elements in the pair

B

the type of the right elements in the pair

MkUPair : (a : A) -> (b : B) -> UPair A B

A pair of elements

a

the left element of the pair

b

the right element of the pair

data Pair : (A : Type) -> (B : Type) -> Type

The non-dependent pair type, also known as conjunction.

A

the type of the left elements in the pair

B

the type of the right elements in the pair

MkPair : (a : A) -> (b : B) -> (A, B)

A pair of elements

a

the left element of the pair

b

the right element of the pair

data DPair : (a : Type) -> (P : a -> Type) -> Type

Dependent pairs aid in the construction of dependent types by
providing evidence that some value resides in the type.

Formally, speaking, dependent pairs represent existential
quantification - they consist of a witness for the existential
claim and a proof that the property holds for it.

a

the value to place in the type.

P

the dependent type that requires the value.

MkDPair : (x : a) -> (pf : P x) -> DPair a P