Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Interaction.Monad

Synopsis

Documentation

data IM a Source #

Interaction monad.

Instances

Instances details
HasOptions IM Source # 
Instance details

Defined in Agda.Interaction.Monad

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

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.