0 | module Data.Linear.LEither
 1 |
 2 | import Data.Linear.Bifunctor
 3 | import Data.Linear.Interface
 4 | import Data.Linear.Notation
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | data LEither : (a, b : Type) -> Type where
10 |   Left : a -@ LEither a b
11 |   Right : b -@ LEither a b
12 |
13 | export
14 | (Consumable a, Consumable b) => Consumable (LEither a b) where
15 |   consume (Left a) = consume a
16 |   consume (Right b) = consume b
17 |
18 | export
19 | (Duplicable a, Duplicable b) => Duplicable (LEither a b) where
20 |   duplicate (Left a) = Left <$> duplicate a
21 |   duplicate (Right b) = Right <$> duplicate b
22 |