Idris2Doc : Data.Rel

# Data.Rel

## Definitions

`Rel : Vect n Type -> Type`
`  Build an n-ary relation type from a Vect of Types`

Totality: total
Visibility: public export
`All : (ts : Vect n Type) -> Rel ts -> Type`
`  Universal quantification of a n-ary Relation over its  arguments to build a (function) type from a `Rel` type    ```  λ> All [Nat,Nat] LTE  (x : Nat) -> (x : Nat) -> LTE x x  ````

Totality: total
Visibility: public export
`Ex : (ts : Vect n Type) -> Rel ts -> Type`
`  Existential quantification of a n-ary relation over its  arguments to build a dependent pair (eg. Sigma type).    Given a (type of) relation `p : [t_1, t_2 ... t_n] x r` where `t_i` and `r` are  types, `Ex` builds the type `Σ (x_1 : t_1). Σ (x_2 : t_2) ... . r`  For example:  ```  λ> Ex [Nat,Nat] LTE  (x : Nat ** (x : Nat ** LTE x x))  ```  Which is the type of a pair of natural numbers along with a proof that the first  is smaller or equal than the second.`

Totality: total
Visibility: public export
`liftRel : (ts : Vect n Type) -> Rel ts -> (Type -> Type) -> Type`
`  Map a type-level function over the co-domain of a n-ary Relation`

Totality: total
Visibility: public export