Idris2Doc : Data.OpenUnion

Data.OpenUnion

This module is inspired by the open union used in the paper
Freer Monads, More Extensible Effects
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