
  0 | module Libraries.Data.IMaybe
  1 | 
  2 | %default total
  3 | 
  4 | public export
  5 | data IMaybe : Bool -> Type -> Type where
  6 |   Nothing : IMaybe False a
  7 |   Just : a -> IMaybe True a
  8 | 
  9 | export
 10 | Functor (IMaybe b) where
 11 |   map f Nothing = Nothing
 12 |   map f (Just x) = Just (f x)
 13 | 
 14 | export
 15 | fromJust : IMaybe True a -> a
 16 | fromJust (Just x) = x
 17 | 
 18 | export
 19 | toList : IMaybe b a -> List a
 20 | toList Nothing = []
 21 | toList (Just x) = [x]
 22 |