
  0 | module Data.Maybe0
  1 | 
  2 | %default total
  3 | 
  4 | ||| An optional data type for erased values.
  5 | ||| At runtime, this is just 0 or 1.
  6 | public export
  7 | data Maybe0 : Type -> Type where
  8 |   Nothing0 : Maybe0 a
  9 |   Just0    : (0 v : a) -> Maybe0 a
 10 | 
 11 | public export
 12 | isJust : Maybe0 a -> Bool
 13 | isJust Nothing0  = False
 14 | isJust (Just0 v) = True
 15 | 
 16 | public export
 17 | map : (0 f : a -> b) -> Maybe0 a -> Maybe0 b
 18 | map f Nothing0  = Nothing0
 19 | map f (Just0 v) = Just0 (f v)
 20 | 
 21 | public export
 22 | data IsJust0 : Maybe0 a -> Type where
 23 |   ItIsJust0 : IsJust0 (Just0 v)
 24 | 
 25 | public export
 26 | 0 fromJust0 : (m : Maybe0 a) -> {auto prf : IsJust0 m} -> a
 27 | fromJust0 (Just0 x) = x
 28 | 
 29 | public export
 30 | (<|>) : Maybe0 t -> Lazy (Maybe0 t) -> Maybe0 t
 31 | (<|>) (Just0 v) _ = Just0 v
 32 | (<|>) Nothing0  m = m
 33 | 
 34 | public export
 35 | zipWith : (0 f : a -> b -> c) -> Maybe0 a -> Maybe0 b -> Maybe0 c
 36 | zipWith f (Just0 x) (Just0 y) = Just0 $ f x y
 37 | zipWith f _         _         = Nothing0
 38 | 
 39 | public export
 40 | zipWith3 : (0 f : a -> b -> c -> d) -> Maybe0 a -> Maybe0 b -> Maybe0 c -> Maybe0 d
 41 | zipWith3 f (Just0 x) (Just0 y) (Just0 z) = Just0 $ f x y z
 42 | zipWith3 f _         _         _         = Nothing0
 43 |