| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Interaction.Monad

Synopsis

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

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

Produced by Haddock version 2.4.2