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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Interaction.Monad

Synopsis

- data IM a
- runIM :: IM a -> TCM a
- readline :: String -> IM (Maybe String)

# Documentation

data IM a Source #

Interaction monad.

#### Instances

Instances details

HasOptions IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods pragmaOptions :: IM PragmaOptions Source # commandLineOptions :: IM CommandLineOptions Source #
MonadTCEnv IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods askTC :: IM TCEnv Source # localTC :: (TCEnv -> TCEnv) -> IM a -> IM a Source #
MonadTCM IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods liftTCM :: TCM a -> IM a Source #
MonadTCState IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods getTC :: IM TCState Source # putTC :: TCState -> IM () Source # modifyTC :: (TCState -> TCState) -> IM () Source #
ReadTCState IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods getTCState :: IM TCState Source # locallyTCState :: Lens' a TCState -> (a -> a) -> IM b -> IM b Source # withTCState :: (TCState -> TCState) -> IM a -> IM a Source #
MonadIO IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods liftIO :: IO a -> IM a Source #
Applicative IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods pure :: a -> IM a Source # (<*>) :: IM (a -> b) -> IM a -> IM b Source # liftA2 :: (a -> b -> c) -> IM a -> IM b -> IM c Source # (*>) :: IM a -> IM b -> IM b Source # (<*) :: IM a -> IM b -> IM a Source #
Functor IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods fmap :: (a -> b) -> IM a -> IM b Source # (<$) :: a -> IM b -> IM a Source #
Monad IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods (>>=) :: IM a -> (a -> IM b) -> IM b Source # (>>) :: IM a -> IM b -> IM b Source # return :: a -> IM a Source #
MonadError TCErr IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods throwError :: TCErr -> IM a Source # catchError :: IM a -> (TCErr -> IM a) -> IM a Source #

runIM :: IM a -> TCM a Source #

readline :: String -> IM (Maybe String) Source #

Line reader. The line reader history is not stored between sessions.