Idris2Doc : Data.OpenUnion

Data.OpenUnion

Union : (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