
  0 | module Libraries.Data.Erased
  1 | 
  2 | %default total
  3 | 
  4 | public export
  5 | record Erased (a : Type) where
  6 |   constructor MkErased
  7 |   0 runErased : a
  8 | 
  9 | export
 10 | Functor Erased where
 11 |   map f (MkErased x) = MkErased (f x)
 12 | 
 13 | export
 14 | Applicative Erased where
 15 |   pure x = MkErased x
 16 |   MkErased f <*> MkErased x = MkErased (f x)
 17 | 
 18 | join : Erased (Erased a) -> Erased a
 19 | join (MkErased mx) = MkErased (let MkErased x = mx in x)
 20 | 
 21 | export
 22 | Monad Erased where
 23 |   mx >>= f = join (f <$> mx)
 24 |