
  0 | module Data.Either0
  1 | 
  2 | %default total
  3 | 
  4 | ||| A choice of two erased values.
  5 | ||| At runtime, this is just 0 or 1.
  6 | public export
  7 | data Either0 : Type -> Type -> Type where
  8 |   Left0  : (0 v : a) -> Either0 a b
  9 |   Right0 : (0 v : b) -> Either0 a b
 10 | 
 11 | ||| This is the identity at runtime.
 12 | public export
 13 | bimap : (0 f : a -> c) -> (0 g : b -> d) -> Either0 a b -> Either0 c d
 14 | bimap f g (Left0 v)  = Left0 $ f v
 15 | bimap f g (Right0 v) = Right0 $ g v
 16 | 
 17 | ||| This is the identity at runtime.
 18 | public export %inline
 19 | map : (0 f : b -> d) -> Either0 a b -> Either0 a d
 20 | map = bimap id
 21 | 
 22 | public export %inline
 23 | 0 either0 : (f : a -> e) -> (g : b -> e) -> Either0 a b -> e
 24 | either0 f g (Left0 v)  = f v
 25 | either0 f g (Right0 v) = g v
 26 | 
 27 | public export
 28 | data IsLeft0 : Either0 a b -> Type where
 29 |   ItIsLeft0 : IsLeft0 (Left0 v)
 30 | 
 31 | public export
 32 | 0 fromLeft0 : (e : Either0 a b) -> {auto prf : IsLeft0 e} -> a
 33 | fromLeft0 (Left0 v) = v
 34 | 
 35 | public export
 36 | data IsRight0 : Either0 a b -> Type where
 37 |   ItIsRight0 : IsRight0 (Right0 v)
 38 | 
 39 | public export
 40 | 0 fromRight0 : (e : Either0 a b) -> {auto prf : IsRight0 e} -> b
 41 | fromRight0 (Right0 v) = v
 42 | 
 43 | public export
 44 | (<|>) : Either0 a b -> Lazy (Either0 a b) -> Either0 a b
 45 | (<|>) (Right0 v) _ = Right0 v
 46 | (<|>) (Left0 _)  e = e
 47 |