Prelude.IO

Definitions

interface HasIO : (Type -> Type) -> Type

Parameters: io
Constraints: Monad io
Constructor: 

MkHasIO

Methods:

liftIO : IO a -> io a

Implementation: 

HasLinearIO io => HasIO io

liftIO : HasIO io => IO a -> io a

Totality: total
Visibility: public export

interface HasLinearIO : (Type -> Type) -> Type

Parameters: io
Constraints: Monad io
Constructor: 

MkHasLinearIO

Methods:

liftIO1 : (1 _ : IO a) -> io a

Implementation: 

HasLinearIO IO

liftIO1 : HasLinearIO io => (1 _ : IO a) -> io a

Totality: total
Visibility: public export

primIO : HasIO io => ((1 _ : %World) -> IORes a) -> io a

Totality: total
Visibility: export

primIO1 : HasLinearIO io => (1 _ : ((1 _ : %World) -> IORes a)) -> io a

Totality: total
Visibility: export

onCollectAny : HasIO io => AnyPtr -> (AnyPtr -> IO ()) -> io GCAnyPtr

Totality: total
Visibility: export

onCollect : HasIO io => Ptr t -> (Ptr t -> IO ()) -> io (GCPtr t)

Totality: total
Visibility: export

prim__getString : Ptr String -> String

putStr : HasIO io => String -> io ()

  Output a string to stdout without a trailing newline.

Totality: total
Visibility: export

putStrLn : HasIO io => String -> io ()

  Output a string to stdout with a trailing newline.

Totality: total
Visibility: export

getLine : HasIO io => io String

  Read one line of input from stdin, without the trailing newline.

Totality: total
Visibility: export

putChar : HasIO io => Char -> io ()

  Write one single-byte character to stdout.

Totality: total
Visibility: export

putCharLn : HasIO io => Char -> io ()

  Write one multi-byte character to stdout, with a trailing newline.

Totality: total
Visibility: export

getChar : HasIO io => io Char

  Read one single-byte character from stdin.

Totality: total
Visibility: export

prim__fork : (1 _ : PrimIO ()) -> PrimIO ThreadID

fork : (1 _ : IO ()) -> IO ThreadID

Totality: total
Visibility: export

prim__threadWait : (1 _ : ThreadID) -> PrimIO ()

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

Totality: total
Visibility: export

print : HasIO io => Show a => a -> io ()

  Output something showable to stdout, without a trailing newline.

Totality: total
Visibility: export

printLn : HasIO io => Show a => a -> io ()

  Output something showable to stdout, with a trailing newline.

Totality: total
Visibility: export