PrimIO

Definitions

data IORes : Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkIORes : a -> (1 _ : %World) -> IORes a

PrimIO : Type -> Type

  Idris's primitive IO, for building abstractions on top of.

Totality: total
Visibility: public export

data IO : Type -> Type

  The internal representation of I/O computations.

Totality: total
Visibility: export
Constructor: 

MkIO : (1 _ : PrimIO a) -> IO a

Hints:

Applicative IO

Functor IO

HasLinearIO IO

Monad IO

prim__io_pure : a -> PrimIO a

Totality: total
Visibility: export

io_pure : a -> IO a

Totality: total
Visibility: export

prim__io_bind : (1 _ : PrimIO a) -> (1 _ : (a -> PrimIO b)) -> PrimIO b

Totality: total
Visibility: export

io_bind : (1 _ : IO a) -> (1 _ : (a -> IO b)) -> IO b

Totality: total
Visibility: export

data Ptr : Type -> Type

Totality: total
Visibility: public export

data AnyPtr : Type

Totality: total
Visibility: public export

data GCPtr : Type -> Type

Totality: total
Visibility: public export

data GCAnyPtr : Type

Totality: total
Visibility: public export

data ThreadID : Type

Totality: total
Visibility: public export

fromPrim : (1 _ : ((1 _ : %World) -> IORes a)) -> IO a

Totality: total
Visibility: export

toPrim : (1 _ : IO a) -> PrimIO a

Totality: total
Visibility: export

prim__nullAnyPtr : AnyPtr -> Int

prim__getNullAnyPtr : AnyPtr

prim__castPtr : AnyPtr -> Ptr t

Totality: total
Visibility: export

prim__forgetPtr : Ptr t -> AnyPtr

Totality: total
Visibility: export

prim__nullPtr : Ptr t -> Int

Totality: total
Visibility: export

unsafePerformIO : IO a -> a

Totality: total
Visibility: export