Agda.Interaction.Monad
type
IM
runIM
readline