Idris2Doc : System

System

dataExitCode : Type
  Programs can either terminate successfully, or end in a caught
failure.

Totality: total
Constructors:
ExitSuccess : ExitCode
  Terminate successfully.
ExitFailure : (errNo : Int) -> So (not (errNo==0)) => ExitCode
  Program terminated for some prescribed reason.

@errNo A non-zero numerical value indicating failure.
@prf Proof that the int value is non-zero.
exitFailure : HasIOio => ioa
  Exit the program indicating failure.

Totality: total
exitSuccess : HasIOio => ioa
  Exit the program after a successful run.

Totality: total
exitWith : HasIOio => ExitCode -> ioa
Totality: total
getArgs : HasIOio => io (ListString)
Totality: total
getEnv : HasIOio => String -> io (MaybeString)
Totality: total
getEnvironment : HasIOio => io (List (String, String))
getPID : HasIOio => ioInt
  Get the ID of the currently running process.

Totality: total
setEnv : HasIOio => String -> String -> Bool -> ioBool
Totality: total
sleep : HasIOio => Int -> io ()
Totality: total
system : HasIOio => String -> ioInt
Totality: total
time : HasIOio => ioInteger
  Return the number of seconds since epoch.

Totality: total
unsetEnv : HasIOio => String -> ioBool
Totality: total
usleep : HasIOio => (x : Int) -> So (x>=0) => io ()
Totality: total