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

Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Monad

Synopsis

type IM = TCMT (InputT IO)
runIM :: IM a -> TCM a
readline :: String -> IM (Maybe String)

Documentation

type IM = TCMT (InputT IO) Source #

Interaction monad.

runIM :: IM a -> TCM a Source #

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

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