- interface HasIO : (Type -> Type) -> Type
- Parameters: io
Constraints: Monad io
Constructor: MkHasIO
Methods:
- liftIO : IO a -> io a
Implementation: - HasLinearIO io => HasIO io
- interface HasLinearIO : (Type -> Type) -> Type
- Parameters: io
Constraints: Monad io
Constructor: MkHasLinearIO
Methods:
- liftIO1 : (1 _ : IO a) -> io a
Implementation: - HasLinearIO IO
- fork : (1 _ : IO ()) -> IO ThreadID
- Totality: total
- getChar : HasIO io => io Char
Read one single-byte character from stdin.
Totality: total- getLine : HasIO io => io String
Read one line of input from stdin, without the trailing newline.
Totality: total- liftIO : HasIO io => IO a -> io a
- Totality: total
- liftIO1 : HasLinearIO io => (1 _ : IO a) -> io a
- Totality: total
- onCollect : HasIO io => Ptr t -> (Ptr t -> IO ()) -> io (GCPtr t)
- Totality: total
- onCollectAny : HasIO io => AnyPtr -> (AnyPtr -> IO ()) -> io GCAnyPtr
- Totality: total
- primIO : HasIO io => ((1 _ : %World) -> IORes a) -> io a
- Totality: total
- primIO1 : HasLinearIO io => (1 _ : ((1 _ : %World) -> IORes a)) -> io a
- Totality: total
- prim__fork : (1 _ : PrimIO ()) -> PrimIO ThreadID
- prim__getString : Ptr String -> String
- prim__threadWait : (1 _ : ThreadID) -> PrimIO ()
- print : (HasIO io, Show a) => a -> io ()
Output something showable to stdout, without a trailing newline.
Totality: total- printLn : (HasIO io, Show a) => a -> io ()
Output something showable to stdout, with a trailing newline.
Totality: total- putChar : HasIO io => Char -> io ()
Write one single-byte character to stdout.
Totality: total- putCharLn : HasIO io => Char -> io ()
Write one multi-byte character to stdout, with a trailing newline.
Totality: total- putStr : HasIO io => String -> io ()
Output a string to stdout without a trailing newline.
Totality: total- putStrLn : HasIO io => String -> io ()
Output a string to stdout with a trailing newline.
Totality: total- threadWait : (1 _ : ThreadID) -> IO ()
- Totality: total