Idris2Doc : Data.Linear.LEither

Data.Linear.LEither

Definitions

data LEither : Type -> Type -> Type
Totality: total
Visibility: public export
Constructors:
Left : a -@ LEither a b
Right : b -@ LEither a b

Hints:
(Consumable a, Consumable b) => Consumable (LEither a b)
(Duplicable a, Duplicable b) => Duplicable (LEither a b)