Agda.Interaction.Monad

Documentation

data IM a

Interaction monad.

Instances

Monad IM

Defined in Agda.Interaction.Monad

Methods

(>>=) :: IM a -> (a -> IM b) -> IM b

(>>) :: IM a -> IM b -> IM b

return :: a -> IM a

Functor IM

Defined in Agda.Interaction.Monad

Methods

fmap :: (a -> b) -> IM a -> IM b

(<$) :: a -> IM b -> IM a

Applicative IM

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

MonadIO IM

Defined in Agda.Interaction.Monad

Methods

liftIO :: IO a -> IM a

HasOptions IM

Defined in Agda.Interaction.Monad

Methods

pragmaOptions :: IM PragmaOptions

commandLineOptions :: IM CommandLineOptions

MonadTCM IM

Defined in Agda.Interaction.Monad

Methods

liftTCM :: TCM a -> IM a

MonadTCState IM

Defined in Agda.Interaction.Monad

Methods

getTC :: IM TCState

putTC :: TCState -> IM ()

modifyTC :: (TCState -> TCState) -> IM ()

MonadTCEnv IM

Defined in Agda.Interaction.Monad

Methods

askTC :: IM TCEnv

localTC :: (TCEnv -> TCEnv) -> IM a -> IM a

ReadTCState IM

Defined in Agda.Interaction.Monad

Methods

getTCState :: IM TCState

locallyTCState :: Lens' a TCState -> (a -> a) -> IM b -> IM b

withTCState :: (TCState -> TCState) -> IM a -> IM a

MonadError TCErr IM

Defined in Agda.Interaction.Monad

Methods

throwError :: TCErr -> IM a

catchError :: IM a -> (TCErr -> IM a) -> IM a

runIM :: IM a -> TCM a

readline :: String -> IM (Maybe String)

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