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 #
Applicative IM Source #
Instance details Defined in Agda.Interaction.Monad Methods pure :: a -> IM a # (<>) :: IM (a -> b) -> IM a -> IM b # liftA2 :: (a -> b -> c) -> IM a -> IM b -> IM c # (>) :: IM a -> IM b -> IM b # (<*) :: IM a -> IM b -> IM a #
Functor IM Source #
Instance details Defined in Agda.Interaction.Monad Methods fmap :: (a -> b) -> IM a -> IM b # (<$) :: a -> IM b -> IM a #
Monad IM Source #
Instance details Defined in Agda.Interaction.Monad Methods (>>=) :: IM a -> (a -> IM b) -> IM b # (>>) :: IM a -> IM b -> IM b # return :: a -> IM a #
MonadError TCErr IM Source #
Instance details Defined in Agda.Interaction.Monad Methods throwError :: TCErr -> IM a catchError :: IM a -> (TCErr -> IM a) -> IM a

runIM :: IM a -> TCM a Source #

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

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