
  0 | module Control.Effect.Lift
  1 | 
  2 | import Control.EffectAlgebra
  3 | 
  4 | namespace Algebra
  5 |   public export
  6 |   [Lift] Monad m => Algebra (Lift m) m where
  7 |     alg ctxx hdl (MkLift x) = x >>= hdl . ( <$ ctxx)
  8 | 
  9 |   %hint public export
 10 |   HintLift : Monad m => Algebra (Lift m) m
 11 |   HintLift = Lift
 12 | 
 13 | ||| Lift a computation to the underlying effect stack.
 14 | public export
 15 | lift : Monad n => Inj (Lift n) sig => Algebra sig m => n a -> m a
 16 | lift x = send {eff = Lift n} $ MkLift (map pure x)
 17 |