Agda-2.4.2.1: A dependently typed functional programming language and proof assistant
Agda.Interaction.Monad
Synopsis
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