Idris2Doc : Data.OpenUnion

# Data.OpenUnion

```This module is inspired by the open union used in the paper
by Oleg Kiselyov and Hiromi Ishii

By using an AtIndex proof, we are able to get rid of all of the unsafe
coercions in the original module.```
dataUnion : (a -> Type) -> Lista -> Type
`  An open union of families is an index picking a family out together with  a value in the family thus picked.`

Totality: total
Constructor:
Element : (k : Nat) -> (0 _ : AtIndexttsk) -> eltt -> Unioneltts
decomp : Unionelt (t::ts) -> Either (Unioneltts) (eltt)
`  We can inspect an open union over a non-empty list of families to check  whether the value it contains belongs either to the first family or any  other in the tail.`

Totality: total
decomp0 : Unionelt [t] -> eltt
`  An open union over a singleton list is just a wrapper`

Totality: total
inj : Membertts => eltt -> Unioneltts
`  Given that equality of type families is not decidable, we have to  rely on the interface `Member` to automatically find the index of a  given family.`

Totality: total
prj : Membertts => Unioneltts -> Maybe (eltt)
`  Given that equality of type families is not decidable, we have to  rely on the interface `Member` to automatically find the index of a  given family.`

Totality: total
split : SubsetNat (HasLengthss) -> Unionelt (ss++ts) -> Either (Unioneltss) (Unioneltts)
`  By doing a bit of arithmetic we can figure out whether the union's value  came from the left or the right list used in the index.`

Totality: total
weakenL : SubsetNat (HasLengthss) -> Unioneltts -> Unionelt (ss++ts)
`  Inserting new union members on the left, requires shifting the index by  the number of members introduced. Note that this number is the only  thing we need to keep around at runtime.`

Totality: total
weakenR : Unioneltts -> Unionelt (ts++us)
`  Inserting new union members on the right leaves the index unchanged.`

Totality: total