Idris2Doc : System.Posix.Errno

System.Posix.Errno

(source)

Reexports

import public System.Posix.Errno.Type
import public Data.Linear.ELift1

Definitions

0 EPrim : Type -> Type
Visibility: public export
toBool : Bits8 -> Bool
  Converts 0 to `False`, everything else to `True`

Visibility: public export
fromNeg : Neg n => Cast n Bits32 => n -> Errno
  Converts a negative number to a system error.

Visibility: export
primMap : (a -> b) -> PrimIO a -> PrimIO b
Visibility: export
elinMap : (a -> b) -> E1 s es a -> E1 s es b
Visibility: export
toVal : (CInt -> a) -> PrimIO CInt -> EPrim a
Visibility: export
toSize : PrimIO SsizeT -> EPrim Bits32
Visibility: export
toUnit : PrimIO CInt -> EPrim ()
Visibility: export
toPidT : PrimIO PidT -> EPrim PidT
Visibility: export
posToUnit : PrimIO Bits32 -> EPrim ()
Visibility: export
posNotErr : Errno -> PrimIO Bits32 -> EPrim Bool
Visibility: export
toRes : PrimIO a -> PrimIO CInt -> EPrim a
Visibility: export
ignore : E1 World es a -> PrimIO ()
Visibility: export
freeFail : Struct f => f World -> Errno -> EPrim b
Visibility: export
finally : PrimIO () -> EPrim a -> EPrim a
Visibility: export
primStruct : (0 f : (Type -> Type)) -> Struct f => SizeOf (f World) => F1 World (f World)
Visibility: export
withStruct : (0 f : (Type -> Type)) -> Struct f => SizeOf (f World) => (f World -> EPrim b) -> EPrim b
Visibility: export
withBox : (0 a : Type) -> SizeOf a => Deref a => (IOBox a -> EPrim b) -> EPrim b
Visibility: export
withPtr : Bits32 -> (AnyPtr -> EPrim b) -> EPrim b
Visibility: export
withCArray : (0 a : Type) -> SizeOf a => (n : Nat) -> (CArrayIO n a -> EPrim b) -> EPrim b
Visibility: export
primTraverse_ : (a -> PrimIO ()) -> List a -> PrimIO ()
Visibility: export
filterM : SnocList a -> (a -> F1 rs Bool) -> List a -> F1 rs (List a)
Visibility: export
values : Deref b => SizeOf b => List c -> CArray s n b -> (b -> F1 s c) -> (k : Nat) -> {auto 0 _ : LTE k n} -> F1 s (List c)
Visibility: export
structs : Struct f => SizeOf (f s) => List c -> CArray s n (f s) -> (f s -> F1 s c) -> (k : Nat) -> {auto 0 _ : LTE k n} -> F1 s (List c)
Visibility: export