Idris2Doc : Prelude.IO

Prelude.IO

Definitions

interfaceHasIO : (Type->Type) ->Type
Parameters: io
Constraints: Monad io
Constructor: 
MkHasIO

Methods:
liftIO : IOa->ioa

Implementation: 
HasLinearIOio=>HasIOio
liftIO : HasIOio=>IOa->ioa
Totality: total
Visibility: public export
interfaceHasLinearIO : (Type->Type) ->Type
Parameters: io
Constraints: Monad io
Constructor: 
MkHasLinearIO

Methods:
liftIO1 : (1_ : IOa) ->ioa

Implementation: 
HasLinearIOIO
liftIO1 : HasLinearIOio=> (1_ : IOa) ->ioa
Totality: total
Visibility: public export
primIO : HasIOio=> ((1_ : %World) ->IOResa) ->ioa
Totality: total
Visibility: export
primIO1 : HasLinearIOio=> (1_ : ((1_ : %World) ->IOResa)) ->ioa
Totality: total
Visibility: export
onCollectAny : HasIOio=>AnyPtr-> (AnyPtr->IO ()) ->ioGCAnyPtr
Totality: total
Visibility: export
onCollect : HasIOio=>Ptrt-> (Ptrt->IO ()) ->io (GCPtrt)
Totality: total
Visibility: export
prim__getString : PtrString->String
putStr : HasIOio=>String->io ()
  Output a string to stdout without a trailing newline.

Totality: total
Visibility: export
putStrLn : HasIOio=>String->io ()
  Output a string to stdout with a trailing newline.

Totality: total
Visibility: export
getLine : HasIOio=>ioString
  Read one line of input from stdin, without the trailing newline.

Totality: total
Visibility: export
putChar : HasIOio=>Char->io ()
  Write one single-byte character to stdout.

Totality: total
Visibility: export
putCharLn : HasIOio=>Char->io ()
  Write one multi-byte character to stdout, with a trailing newline.

Totality: total
Visibility: export
getChar : HasIOio=>ioChar
  Read one single-byte character from stdin.

Totality: total
Visibility: export
prim__fork : (1_ : PrimIO ()) ->PrimIOThreadID
fork : (1_ : IO ()) ->IOThreadID
Totality: total
Visibility: export
prim__threadWait : (1_ : ThreadID) ->PrimIO ()
threadWait : (1_ : ThreadID) ->IO ()
Totality: total
Visibility: export
print : HasIOio=>Showa=>a->io ()
  Output something showable to stdout, without a trailing newline.

Totality: total
Visibility: export
printLn : HasIOio=>Showa=>a->io ()
  Output something showable to stdout, with a trailing newline.

Totality: total
Visibility: export