Idris2Doc : Prelude.IO

Prelude.IO

interfaceHasIO : (Type -> Type) -> Type
Parameters: io
Constraints: Monad io
Constructor: MkHasIO
Methods:
liftIO : IOa -> ioa

Implementation: 
HasLinearIOio => HasIOio
interfaceHasLinearIO : (Type -> Type) -> Type
Parameters: io
Constraints: Monad io
Constructor: MkHasLinearIO
Methods:
liftIO1 : (1 _ : IOa) -> ioa

Implementation: 
HasLinearIOIO
fork : (1 _ : IO ()) -> IOThreadID
Totality: total
getChar : HasIOio => ioChar
  Read one single-byte character from stdin.

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

Totality: total
liftIO : HasIOio => IOa -> ioa
Totality: total
liftIO1 : HasLinearIOio => (1 _ : IOa) -> ioa
Totality: total
onCollect : HasIOio => Ptrt -> (Ptrt -> IO ()) -> io (GCPtrt)
Totality: total
onCollectAny : HasIOio => AnyPtr -> (AnyPtr -> IO ()) -> ioGCAnyPtr
Totality: total
primIO : HasIOio => ((1 _ : %World) -> IOResa) -> ioa
Totality: total
primIO1 : HasLinearIOio => (1 _ : ((1 _ : %World) -> IOResa)) -> ioa
Totality: total
prim__fork : (1 _ : PrimIO ()) -> PrimIOThreadID
prim__getString : PtrString -> String
prim__threadWait : (1 _ : ThreadID) -> PrimIO ()
print : (HasIOio, Showa) => a -> io ()
  Output something showable to stdout, without a trailing newline.

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

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

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

Totality: total
putStr : HasIOio => String -> io ()
  Output a string to stdout without a trailing newline.

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

Totality: total
threadWait : (1 _ : ThreadID) -> IO ()
Totality: total