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

Safe HaskellNone
LanguageHaskell98

Agda.Interaction.Monad

Synopsis

Documentation

type IM = TCMT (InputT IO) Source

Interaction monad.

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

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

runIM :: IM a -> TCM a Source