Agda-2.8.0: A dependently typed functional programming language and proof assistant

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

type CommandM = CommandM' TCM Source #

localStateCommandM :: CommandM a -> CommandM a Source #

Restore both `TCState` and `CommandState`.

liftLocalState :: TCM a -> CommandM a Source #

Restore `TCState`, do not touch `CommandState`.

revLift Source #

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.

revLiftTC Source #

Arguments

:: MonadTCState m |
=> (forall c. m c -> TCState -> k (c, TCState)) | run
-> (forall b. k b -> m b) | lift
-> (forall x. (m a -> k x) -> k x) |
-> m a | reverse lift in double negative position