| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Command
Synopsis
- type CommandM = CommandM' TCM
- localStateCommandM :: CommandM a -> CommandM a
- liftLocalState :: TCM a -> CommandM a
- revLift :: MonadState st m => (forall c. m c -> st -> k (c, st)) -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
- revLiftTC :: MonadTCState m => (forall c. m c -> TCState -> k (c, TCState)) -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
Documentation
Arguments
| :: MonadState st m | |
| => (forall c. m c -> st -> k (c, st)) | run |
| -> (forall b. k b -> m b) | lift |
| -> (forall x. (m a -> k x) -> k x) | |
| -> m a | reverse lift in double negative position |
Build an opposite action to lift for state monads.