Portability | see LANGUAGE pragmas (... GHC) |
---|---|

Stability | experimental |

Maintainer | nicolas.frisby@gmail.com |

Finite sums of types.

# Documentation

(Med m (LeftmostRange ts) ~ Med m (LeftmostRange us), Reduce m ts, Reduce m us) => Reduce m (:+ ts us) | |

(c ::: (All u), d ::: (All u)) => (:+ c d) ::: (All u) | |

d ::: (:? (Exists p) path) => (:+ c d) ::: (:? (Exists p) (OnRight path)) | |

c ::: (:? (Exists p) path) => (:+ c d) ::: (:? (Exists p) (OnLeft path)) |

The higher-order universe `All`

. `c`

inhabits `All u`

if `c`

is a type-sum
and all types in it inhabit `u`

.

The higher-order universe `Exists`

. `c`

inhabits `Exists p`

if there
exists a type `t`

in the type-sum `c`

for which

. NB
that `True`

~ `Pred`

p t`c`

is not necessarily a type-sum; i.e. there is no well-typed total
function from `Exists p c`

to `TSum c`

.